YES 7.931
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule List
|
| ((group :: Eq a => [a] -> [[a]]) :: Eq a => [a] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | group :: Eq a => [a] -> [[a]]
|
| | groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
| groupBy | _ [] | = | [] |
| groupBy | eq (x : xs) | = |
| (x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Lambda Reductions:
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
mainModule List
|
| ((group :: Eq a => [a] -> [[a]]) :: Eq a => [a] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | group :: Eq a => [a] -> [[a]]
|
| | groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
| groupBy | _ [] | = | [] |
| groupBy | eq (x : xs) | = |
| (x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xs@(ww : wx)
is replaced by the following term
ww : wx
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
|
| ((group :: Eq a => [a] -> [[a]]) :: Eq a => [a] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | group :: Eq a => [a] -> [[a]]
|
| | groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
| groupBy | vw [] | = | [] |
| groupBy | eq (x : xs) | = |
| (x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
| undefined0 | True | = undefined |
| undefined1 | | = undefined0 False |
The following Function with conditions
| span | p [] | = ([],[]) |
| span | p (ww : wx) | |
is transformed to
| span | p [] | = span3 p [] |
| span | p (ww : wx) | = span2 p (ww : wx) |
| span2 | p (ww : wx) | =
| span1 p ww wx (p ww) |
| where |
| span0 | p ww wx True | = ([],ww : wx) |
|
|
| span1 | p ww wx True | = (ww : ys,zs) |
| span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
|
| span3 | p [] | = ([],[]) |
| span3 | yz zu | = span2 yz zu |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule List
|
| ((group :: Eq a => [a] -> [[a]]) :: Eq a => [a] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | group :: Eq a => [a] -> [[a]]
|
| | groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
| groupBy | vw [] | = | [] |
| groupBy | eq (x : xs) | = |
| (x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Let/Where Reductions:
The bindings of the following Let/Where expression
| (x : ys) : groupBy eq zs |
| where | |
| |
| |
| |
| |
are unpacked to the following functions on top level
| groupByYs0 | zv zw zx (ys,vx) | = ys |
| groupByZs | zv zw zx | = groupByZs0 zv zw zx (groupByVv10 zv zw zx) |
| groupByVv10 | zv zw zx | = span (zv zw) zx |
| groupByYs | zv zw zx | = groupByYs0 zv zw zx (groupByVv10 zv zw zx) |
| groupByZs0 | zv zw zx (vy,zs) | = zs |
The bindings of the following Let/Where expression
| span1 p ww wx (p ww) |
| where |
| span0 | p ww wx True | = ([],ww : wx) |
|
|
| span1 | p ww wx True | = (ww : ys,zs) |
| span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
are unpacked to the following functions on top level
| span2Zs1 | zy zz (wy,zs) | = zs |
| span2Ys1 | zy zz (ys,wz) | = ys |
| span2Span1 | zy zz p ww wx True | = (ww : span2Ys zy zz,span2Zs zy zz) |
| span2Span1 | zy zz p ww wx False | = span2Span0 zy zz p ww wx otherwise |
| span2Vu43 | zy zz | = span zy zz |
| span2Ys | zy zz | = span2Ys1 zy zz (span2Vu43 zy zz) |
| span2Span0 | zy zz p ww wx True | = ([],ww : wx) |
| span2Zs | zy zz | = span2Zs1 zy zz (span2Vu43 zy zz) |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
mainModule List
|
| (group :: Eq a => [a] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | group :: Eq a => [a] -> [[a]]
|
| | groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
| groupBy | vw [] | = | [] |
| groupBy | eq (x : xs) | = | (x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs) |
|
| |
| groupByVv10 | zv zw zx | = | span (zv zw) zx |
|
| |
| groupByYs | zv zw zx | = | groupByYs0 zv zw zx (groupByVv10 zv zw zx) |
|
| |
| groupByYs0 | zv zw zx (ys,vx) | = | ys |
|
| |
| groupByZs | zv zw zx | = | groupByZs0 zv zw zx (groupByVv10 zv zw zx) |
|
| |
| groupByZs0 | zv zw zx (vy,zs) | = | zs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(vuu5700), Succ(vuu3101000)) → new_primPlusNat(vuu5700, vuu3101000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(vuu5700), Succ(vuu3101000)) → new_primPlusNat(vuu5700, vuu3101000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(vuu30100), Succ(vuu310100)) → new_primMulNat(vuu30100, Succ(vuu310100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(vuu30100), Succ(vuu310100)) → new_primMulNat(vuu30100, Succ(vuu310100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(vuu3000), Succ(vuu31000)) → new_primEqNat(vuu3000, vuu31000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(vuu3000), Succ(vuu31000)) → new_primEqNat(vuu3000, vuu31000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), app(app(ty_@2, cc), cd), ce) → new_esEs(vuu300, vuu3100, cc, cd)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, app(app(app(ty_@3, gg), gh), ha), ge) → new_esEs1(vuu301, vuu3101, gg, gh, ha)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, eh, app(app(ty_Either, fh), ga)) → new_esEs2(vuu302, vuu3102, fh, ga)
new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), app(ty_Maybe, bde)) → new_esEs0(vuu300, vuu3100, bde)
new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), app(ty_[], bec)) → new_esEs3(vuu300, vuu3100, bec)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, app(app(ty_@2, gc), gd), ge) → new_esEs(vuu301, vuu3101, gc, gd)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), app(app(ty_Either, bac), bad), eh, ge) → new_esEs2(vuu300, vuu3100, bac, bad)
new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), app(app(ty_@2, bdc), bdd)) → new_esEs(vuu300, vuu3100, bdc, bdd)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, eh, app(ty_[], gb)) → new_esEs3(vuu302, vuu3102, gb)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, app(ty_Maybe, gf), ge) → new_esEs0(vuu301, vuu3101, gf)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, eh, app(app(app(ty_@3, fd), ff), fg)) → new_esEs1(vuu302, vuu3102, fd, ff, fg)
new_esEs0(Just(vuu300), Just(vuu3100), app(ty_Maybe, dh)) → new_esEs0(vuu300, vuu3100, dh)
new_esEs2(Left(vuu300), Left(vuu3100), app(app(ty_Either, bbe), bbf), bah) → new_esEs2(vuu300, vuu3100, bbe, bbf)
new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), ba, app(ty_Maybe, bd)) → new_esEs0(vuu301, vuu3101, bd)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, app(app(ty_Either, hb), hc), ge) → new_esEs2(vuu301, vuu3101, hb, hc)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, eh, app(ty_Maybe, fc)) → new_esEs0(vuu302, vuu3102, fc)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, eh, app(app(ty_@2, fa), fb)) → new_esEs(vuu302, vuu3102, fa, fb)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), app(ty_[], bae), eh, ge) → new_esEs3(vuu300, vuu3100, bae)
new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), bdb) → new_esEs3(vuu301, vuu3101, bdb)
new_esEs2(Right(vuu300), Right(vuu3100), bbh, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs1(vuu300, vuu3100, bcd, bce, bcf)
new_esEs2(Left(vuu300), Left(vuu3100), app(ty_[], bbg), bah) → new_esEs3(vuu300, vuu3100, bbg)
new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), ba, app(app(app(ty_@3, be), bf), bg)) → new_esEs1(vuu301, vuu3101, be, bf, bg)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), app(app(app(ty_@3, hh), baa), bab), eh, ge) → new_esEs1(vuu300, vuu3100, hh, baa, bab)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, app(ty_[], hd), ge) → new_esEs3(vuu301, vuu3101, hd)
new_esEs0(Just(vuu300), Just(vuu3100), app(app(ty_@2, df), dg)) → new_esEs(vuu300, vuu3100, df, dg)
new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), app(ty_Maybe, cf), ce) → new_esEs0(vuu300, vuu3100, cf)
new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), ba, app(ty_[], cb)) → new_esEs3(vuu301, vuu3101, cb)
new_esEs2(Left(vuu300), Left(vuu3100), app(app(app(ty_@3, bbb), bbc), bbd), bah) → new_esEs1(vuu300, vuu3100, bbb, bbc, bbd)
new_esEs0(Just(vuu300), Just(vuu3100), app(ty_[], ef)) → new_esEs3(vuu300, vuu3100, ef)
new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), ba, app(app(ty_Either, bh), ca)) → new_esEs2(vuu301, vuu3101, bh, ca)
new_esEs2(Right(vuu300), Right(vuu3100), bbh, app(app(ty_@2, bca), bcb)) → new_esEs(vuu300, vuu3100, bca, bcb)
new_esEs2(Right(vuu300), Right(vuu3100), bbh, app(app(ty_Either, bcg), bch)) → new_esEs2(vuu300, vuu3100, bcg, bch)
new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), ba, app(app(ty_@2, bb), bc)) → new_esEs(vuu301, vuu3101, bb, bc)
new_esEs2(Left(vuu300), Left(vuu3100), app(app(ty_@2, baf), bag), bah) → new_esEs(vuu300, vuu3100, baf, bag)
new_esEs2(Right(vuu300), Right(vuu3100), bbh, app(ty_[], bda)) → new_esEs3(vuu300, vuu3100, bda)
new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), app(app(ty_Either, bea), beb)) → new_esEs2(vuu300, vuu3100, bea, beb)
new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), app(app(ty_Either, dc), dd), ce) → new_esEs2(vuu300, vuu3100, dc, dd)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), app(ty_Maybe, hg), eh, ge) → new_esEs0(vuu300, vuu3100, hg)
new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), app(app(app(ty_@3, cg), da), db), ce) → new_esEs1(vuu300, vuu3100, cg, da, db)
new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), app(app(ty_@2, he), hf), eh, ge) → new_esEs(vuu300, vuu3100, he, hf)
new_esEs2(Left(vuu300), Left(vuu3100), app(ty_Maybe, bba), bah) → new_esEs0(vuu300, vuu3100, bba)
new_esEs2(Right(vuu300), Right(vuu3100), bbh, app(ty_Maybe, bcc)) → new_esEs0(vuu300, vuu3100, bcc)
new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), app(ty_[], de), ce) → new_esEs3(vuu300, vuu3100, de)
new_esEs0(Just(vuu300), Just(vuu3100), app(app(ty_Either, ed), ee)) → new_esEs2(vuu300, vuu3100, ed, ee)
new_esEs0(Just(vuu300), Just(vuu3100), app(app(app(ty_@3, ea), eb), ec)) → new_esEs1(vuu300, vuu3100, ea, eb, ec)
new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(vuu300, vuu3100, bdf, bdg, bdh)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), app(app(ty_@2, bdc), bdd)) → new_esEs(vuu300, vuu3100, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(vuu300), Just(vuu3100), app(app(ty_@2, df), dg)) → new_esEs(vuu300, vuu3100, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(vuu300, vuu3100, bdf, bdg, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(vuu300), Just(vuu3100), app(app(app(ty_@3, ea), eb), ec)) → new_esEs1(vuu300, vuu3100, ea, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(vuu300), Just(vuu3100), app(ty_[], ef)) → new_esEs3(vuu300, vuu3100, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), app(ty_Maybe, bde)) → new_esEs0(vuu300, vuu3100, bde)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), app(app(ty_Either, bea), beb)) → new_esEs2(vuu300, vuu3100, bea, beb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(vuu300), Just(vuu3100), app(ty_Maybe, dh)) → new_esEs0(vuu300, vuu3100, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(vuu300), Just(vuu3100), app(app(ty_Either, ed), ee)) → new_esEs2(vuu300, vuu3100, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), app(app(ty_@2, cc), cd), ce) → new_esEs(vuu300, vuu3100, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), ba, app(app(ty_@2, bb), bc)) → new_esEs(vuu301, vuu3101, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), ba, app(app(app(ty_@3, be), bf), bg)) → new_esEs1(vuu301, vuu3101, be, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), app(app(app(ty_@3, cg), da), db), ce) → new_esEs1(vuu300, vuu3100, cg, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), ba, app(ty_[], cb)) → new_esEs3(vuu301, vuu3101, cb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), app(ty_[], de), ce) → new_esEs3(vuu300, vuu3100, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), ba, app(ty_Maybe, bd)) → new_esEs0(vuu301, vuu3101, bd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), app(ty_Maybe, cf), ce) → new_esEs0(vuu300, vuu3100, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), ba, app(app(ty_Either, bh), ca)) → new_esEs2(vuu301, vuu3101, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(vuu300, vuu301), @2(vuu3100, vuu3101), app(app(ty_Either, dc), dd), ce) → new_esEs2(vuu300, vuu3100, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, app(app(ty_@2, gc), gd), ge) → new_esEs(vuu301, vuu3101, gc, gd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, eh, app(app(ty_@2, fa), fb)) → new_esEs(vuu302, vuu3102, fa, fb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), app(app(ty_@2, he), hf), eh, ge) → new_esEs(vuu300, vuu3100, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(vuu300), Right(vuu3100), bbh, app(app(ty_@2, bca), bcb)) → new_esEs(vuu300, vuu3100, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(vuu300), Left(vuu3100), app(app(ty_@2, baf), bag), bah) → new_esEs(vuu300, vuu3100, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, app(app(app(ty_@3, gg), gh), ha), ge) → new_esEs1(vuu301, vuu3101, gg, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, eh, app(app(app(ty_@3, fd), ff), fg)) → new_esEs1(vuu302, vuu3102, fd, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), app(app(app(ty_@3, hh), baa), bab), eh, ge) → new_esEs1(vuu300, vuu3100, hh, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, eh, app(ty_[], gb)) → new_esEs3(vuu302, vuu3102, gb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), app(ty_[], bae), eh, ge) → new_esEs3(vuu300, vuu3100, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, app(ty_[], hd), ge) → new_esEs3(vuu301, vuu3101, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, app(ty_Maybe, gf), ge) → new_esEs0(vuu301, vuu3101, gf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, eh, app(ty_Maybe, fc)) → new_esEs0(vuu302, vuu3102, fc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), app(ty_Maybe, hg), eh, ge) → new_esEs0(vuu300, vuu3100, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, eh, app(app(ty_Either, fh), ga)) → new_esEs2(vuu302, vuu3102, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), app(app(ty_Either, bac), bad), eh, ge) → new_esEs2(vuu300, vuu3100, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), eg, app(app(ty_Either, hb), hc), ge) → new_esEs2(vuu301, vuu3101, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Right(vuu300), Right(vuu3100), bbh, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs1(vuu300, vuu3100, bcd, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(Left(vuu300), Left(vuu3100), app(app(app(ty_@3, bbb), bbc), bbd), bah) → new_esEs1(vuu300, vuu3100, bbb, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(vuu300), Left(vuu3100), app(ty_[], bbg), bah) → new_esEs3(vuu300, vuu3100, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(vuu300), Right(vuu3100), bbh, app(ty_[], bda)) → new_esEs3(vuu300, vuu3100, bda)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(vuu300), Left(vuu3100), app(ty_Maybe, bba), bah) → new_esEs0(vuu300, vuu3100, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(vuu300), Right(vuu3100), bbh, app(ty_Maybe, bcc)) → new_esEs0(vuu300, vuu3100, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(vuu300), Left(vuu3100), app(app(ty_Either, bbe), bbf), bah) → new_esEs2(vuu300, vuu3100, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(vuu300), Right(vuu3100), bbh, app(app(ty_Either, bcg), bch)) → new_esEs2(vuu300, vuu3100, bcg, bch)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), app(ty_[], bec)) → new_esEs3(vuu300, vuu3100, bec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(:(vuu300, vuu301), :(vuu3100, vuu3101), bdb) → new_esEs3(vuu301, vuu3101, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs1(vuu49, vuu50, vuu51, True, bc) → new_span2Zs(vuu49, vuu51, bc)
new_span2Zs1(vuu49, vuu50, vuu51, True, bc) → new_span2Ys(vuu49, vuu51, bc)
new_span2Ys1(vuu40, vuu41, vuu42, True, ba) → new_span2Zs(vuu40, vuu42, ba)
new_span2Ys(vuu9, :(vuu110, vuu111), bd) → new_span2Ys1(vuu9, vuu110, vuu111, new_esEs5(vuu9, vuu110, bd), bd)
new_span2Ys1(vuu40, vuu41, vuu42, True, ba) → new_span2Ys(vuu40, vuu42, ba)
new_span2Zs(vuu18, :(vuu200, vuu201), bb) → new_span2Zs1(vuu18, vuu200, vuu201, new_esEs4(vuu18, vuu200, bb), bb)
The TRS R consists of the following rules:
new_esEs4(vuu18, vuu200, app(app(app(ty_@3, ca), cb), cc)) → new_esEs14(vuu18, vuu200, ca, cb, cc)
new_esEs22(vuu300, vuu3100, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs21(vuu301, vuu3101, ty_@0) → new_esEs13(vuu301, vuu3101)
new_esEs19(False, True) → False
new_esEs19(True, False) → False
new_esEs5(vuu9, vuu110, app(ty_Ratio, ee)) → new_esEs11(vuu9, vuu110, ee)
new_esEs27(vuu300, vuu3100, app(ty_[], caf)) → new_esEs16(vuu300, vuu3100, caf)
new_primPlusNat1(Succ(vuu5700), Succ(vuu3101000)) → Succ(Succ(new_primPlusNat1(vuu5700, vuu3101000)))
new_esEs25(vuu302, vuu3102, app(ty_[], bgb)) → new_esEs16(vuu302, vuu3102, bgb)
new_esEs21(vuu301, vuu3101, ty_Double) → new_esEs17(vuu301, vuu3101)
new_primEqInt(Pos(Succ(vuu3000)), Neg(vuu3100)) → False
new_primEqInt(Neg(Succ(vuu3000)), Pos(vuu3100)) → False
new_esEs25(vuu302, vuu3102, ty_Bool) → new_esEs19(vuu302, vuu3102)
new_esEs25(vuu302, vuu3102, app(ty_Ratio, bfc)) → new_esEs11(vuu302, vuu3102, bfc)
new_esEs25(vuu302, vuu3102, ty_Char) → new_esEs8(vuu302, vuu3102)
new_esEs25(vuu302, vuu3102, ty_@0) → new_esEs13(vuu302, vuu3102)
new_esEs15(Left(vuu300), Right(vuu3100), ha, ff) → False
new_esEs15(Right(vuu300), Left(vuu3100), ha, ff) → False
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(app(ty_Either, baa), bab)) → new_esEs15(vuu300, vuu3100, baa, bab)
new_esEs18(Float(vuu300, vuu301), Float(vuu3100, vuu3101)) → new_esEs9(new_sr(vuu300, vuu3100), new_sr(vuu301, vuu3101))
new_esEs26(vuu301, vuu3101, ty_Int) → new_esEs9(vuu301, vuu3101)
new_esEs27(vuu300, vuu3100, app(ty_Ratio, bhg)) → new_esEs11(vuu300, vuu3100, bhg)
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(ty_Ratio, hd)) → new_esEs11(vuu300, vuu3100, hd)
new_primEqInt(Pos(Zero), Neg(Succ(vuu31000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vuu31000))) → False
new_esEs13(@0, @0) → True
new_esEs12(Just(vuu300), Just(vuu3100), app(app(ty_@2, bdd), bde)) → new_esEs7(vuu300, vuu3100, bdd, bde)
new_esEs27(vuu300, vuu3100, app(app(ty_@2, bhe), bhf)) → new_esEs7(vuu300, vuu3100, bhe, bhf)
new_esEs20(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), app(app(ty_Either, gf), gg), ff) → new_esEs15(vuu300, vuu3100, gf, gg)
new_esEs26(vuu301, vuu3101, app(ty_Maybe, bgf)) → new_esEs12(vuu301, vuu3101, bgf)
new_esEs22(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_primMulNat0(Zero, Zero) → Zero
new_esEs22(vuu300, vuu3100, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs21(vuu301, vuu3101, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs14(vuu301, vuu3101, bbb, bbc, bbd)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Float, ff) → new_esEs18(vuu300, vuu3100)
new_esEs7(@2(vuu300, vuu301), @2(vuu3100, vuu3101), bad, bae) → new_asAs(new_esEs22(vuu300, vuu3100, bad), new_esEs21(vuu301, vuu3101, bae))
new_esEs26(vuu301, vuu3101, app(ty_[], bhd)) → new_esEs16(vuu301, vuu3101, bhd)
new_esEs21(vuu301, vuu3101, app(app(ty_Either, bbe), bbf)) → new_esEs15(vuu301, vuu3101, bbe, bbf)
new_primPlusNat0(Zero, vuu310100) → Succ(vuu310100)
new_esEs4(vuu18, vuu200, ty_Ordering) → new_esEs10(vuu18, vuu200)
new_esEs6(Integer(vuu300), Integer(vuu3100)) → new_primEqInt(vuu300, vuu3100)
new_esEs4(vuu18, vuu200, app(ty_Ratio, bg)) → new_esEs11(vuu18, vuu200, bg)
new_esEs5(vuu9, vuu110, app(app(app(ty_@3, eg), eh), fa)) → new_esEs14(vuu9, vuu110, eg, eh, fa)
new_esEs25(vuu302, vuu3102, ty_Float) → new_esEs18(vuu302, vuu3102)
new_esEs16(:(vuu300, vuu301), :(vuu3100, vuu3101), cg) → new_asAs(new_esEs20(vuu300, vuu3100, cg), new_esEs16(vuu301, vuu3101, cg))
new_esEs26(vuu301, vuu3101, ty_Ordering) → new_esEs10(vuu301, vuu3101)
new_sr(Pos(vuu3010), Neg(vuu31010)) → Neg(new_primMulNat0(vuu3010, vuu31010))
new_sr(Neg(vuu3010), Pos(vuu31010)) → Neg(new_primMulNat0(vuu3010, vuu31010))
new_esEs15(Left(vuu300), Left(vuu3100), ty_Char, ff) → new_esEs8(vuu300, vuu3100)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs25(vuu302, vuu3102, app(app(ty_Either, bfh), bga)) → new_esEs15(vuu302, vuu3102, bfh, bga)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Int, ff) → new_esEs9(vuu300, vuu3100)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, ty_Integer) → new_esEs6(vuu9, vuu110)
new_esEs12(Just(vuu300), Just(vuu3100), ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, app(ty_Ratio, dc)) → new_esEs11(vuu300, vuu3100, dc)
new_esEs12(Just(vuu300), Just(vuu3100), app(app(ty_Either, bec), bed)) → new_esEs15(vuu300, vuu3100, bec, bed)
new_esEs22(vuu300, vuu3100, app(ty_[], bda)) → new_esEs16(vuu300, vuu3100, bda)
new_esEs26(vuu301, vuu3101, ty_Float) → new_esEs18(vuu301, vuu3101)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs14(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), bef, beg, beh) → new_asAs(new_esEs27(vuu300, vuu3100, bef), new_asAs(new_esEs26(vuu301, vuu3101, beg), new_esEs25(vuu302, vuu3102, beh)))
new_esEs12(Just(vuu300), Just(vuu3100), ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs26(vuu301, vuu3101, ty_Integer) → new_esEs6(vuu301, vuu3101)
new_esEs4(vuu18, vuu200, app(app(ty_Either, cd), ce)) → new_esEs15(vuu18, vuu200, cd, ce)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Double, ff) → new_esEs17(vuu300, vuu3100)
new_primEqNat0(Zero, Succ(vuu31000)) → False
new_primEqNat0(Succ(vuu3000), Zero) → False
new_esEs21(vuu301, vuu3101, ty_Int) → new_esEs9(vuu301, vuu3101)
new_esEs26(vuu301, vuu3101, app(app(ty_@2, bgc), bgd)) → new_esEs7(vuu301, vuu3101, bgc, bgd)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs4(vuu18, vuu200, ty_Float) → new_esEs18(vuu18, vuu200)
new_esEs25(vuu302, vuu3102, app(app(ty_@2, bfa), bfb)) → new_esEs7(vuu302, vuu3102, bfa, bfb)
new_esEs4(vuu18, vuu200, ty_Bool) → new_esEs19(vuu18, vuu200)
new_esEs23(vuu301, vuu3101, ty_Integer) → new_esEs6(vuu301, vuu3101)
new_esEs22(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs21(vuu301, vuu3101, app(ty_Maybe, bba)) → new_esEs12(vuu301, vuu3101, bba)
new_esEs16(:(vuu300, vuu301), [], cg) → False
new_esEs16([], :(vuu3100, vuu3101), cg) → False
new_esEs5(vuu9, vuu110, ty_Ordering) → new_esEs10(vuu9, vuu110)
new_esEs5(vuu9, vuu110, ty_Float) → new_esEs18(vuu9, vuu110)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs26(vuu301, vuu3101, ty_@0) → new_esEs13(vuu301, vuu3101)
new_esEs15(Left(vuu300), Left(vuu3100), app(ty_[], gh), ff) → new_esEs16(vuu300, vuu3100, gh)
new_esEs24(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_esEs27(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs25(vuu302, vuu3102, ty_Integer) → new_esEs6(vuu302, vuu3102)
new_esEs26(vuu301, vuu3101, ty_Char) → new_esEs8(vuu301, vuu3101)
new_esEs21(vuu301, vuu3101, ty_Float) → new_esEs18(vuu301, vuu3101)
new_esEs4(vuu18, vuu200, ty_@0) → new_esEs13(vuu18, vuu200)
new_esEs26(vuu301, vuu3101, ty_Double) → new_esEs17(vuu301, vuu3101)
new_esEs4(vuu18, vuu200, ty_Integer) → new_esEs6(vuu18, vuu200)
new_esEs12(Just(vuu300), Just(vuu3100), app(ty_Ratio, bdf)) → new_esEs11(vuu300, vuu3100, bdf)
new_esEs22(vuu300, vuu3100, ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs25(vuu302, vuu3102, ty_Double) → new_esEs17(vuu302, vuu3102)
new_sr(Neg(vuu3010), Neg(vuu31010)) → Pos(new_primMulNat0(vuu3010, vuu31010))
new_esEs10(LT, LT) → True
new_esEs10(GT, EQ) → False
new_esEs10(EQ, GT) → False
new_esEs27(vuu300, vuu3100, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, app(ty_[], eb)) → new_esEs16(vuu300, vuu3100, eb)
new_esEs12(Just(vuu300), Nothing, bdc) → False
new_esEs12(Nothing, Just(vuu3100), bdc) → False
new_asAs(False, vuu34) → False
new_sr(Pos(vuu3010), Pos(vuu31010)) → Pos(new_primMulNat0(vuu3010, vuu31010))
new_esEs27(vuu300, vuu3100, app(ty_Maybe, bhh)) → new_esEs12(vuu300, vuu3100, bhh)
new_primEqNat0(Zero, Zero) → True
new_esEs20(vuu300, vuu3100, app(ty_Maybe, dd)) → new_esEs12(vuu300, vuu3100, dd)
new_primMulNat0(Succ(vuu30100), Zero) → Zero
new_primMulNat0(Zero, Succ(vuu310100)) → Zero
new_esEs15(Left(vuu300), Left(vuu3100), app(app(app(ty_@3, gc), gd), ge), ff) → new_esEs14(vuu300, vuu3100, gc, gd, ge)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Integer, ff) → new_esEs6(vuu300, vuu3100)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs25(vuu302, vuu3102, ty_Ordering) → new_esEs10(vuu302, vuu3102)
new_esEs10(GT, GT) → True
new_esEs15(Left(vuu300), Left(vuu3100), app(ty_Maybe, gb), ff) → new_esEs12(vuu300, vuu3100, gb)
new_esEs23(vuu301, vuu3101, ty_Int) → new_esEs9(vuu301, vuu3101)
new_esEs4(vuu18, vuu200, app(ty_Maybe, bh)) → new_esEs12(vuu18, vuu200, bh)
new_esEs22(vuu300, vuu3100, app(app(ty_@2, bbh), bca)) → new_esEs7(vuu300, vuu3100, bbh, bca)
new_esEs12(Nothing, Nothing, bdc) → True
new_esEs19(True, True) → True
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(ty_[], bac)) → new_esEs16(vuu300, vuu3100, bac)
new_esEs27(vuu300, vuu3100, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs27(vuu300, vuu3100, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(app(app(ty_@3, hf), hg), hh)) → new_esEs14(vuu300, vuu3100, hf, hg, hh)
new_esEs5(vuu9, vuu110, ty_@0) → new_esEs13(vuu9, vuu110)
new_esEs5(vuu9, vuu110, ty_Int) → new_esEs9(vuu9, vuu110)
new_primPlusNat0(Succ(vuu570), vuu310100) → Succ(Succ(new_primPlusNat1(vuu570, vuu310100)))
new_esEs20(vuu300, vuu3100, app(app(app(ty_@3, de), df), dg)) → new_esEs14(vuu300, vuu3100, de, df, dg)
new_esEs25(vuu302, vuu3102, app(ty_Maybe, bfd)) → new_esEs12(vuu302, vuu3102, bfd)
new_esEs15(Left(vuu300), Left(vuu3100), app(ty_Ratio, ga), ff) → new_esEs11(vuu300, vuu3100, ga)
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(app(ty_@2, hb), hc)) → new_esEs7(vuu300, vuu3100, hb, hc)
new_esEs15(Left(vuu300), Left(vuu3100), ty_@0, ff) → new_esEs13(vuu300, vuu3100)
new_esEs10(EQ, EQ) → True
new_primEqInt(Neg(Succ(vuu3000)), Neg(Succ(vuu31000))) → new_primEqNat0(vuu3000, vuu31000)
new_esEs4(vuu18, vuu200, ty_Double) → new_esEs17(vuu18, vuu200)
new_esEs27(vuu300, vuu3100, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs21(vuu301, vuu3101, ty_Ordering) → new_esEs10(vuu301, vuu3101)
new_primPlusNat1(Zero, Succ(vuu3101000)) → Succ(vuu3101000)
new_primPlusNat1(Succ(vuu5700), Zero) → Succ(vuu5700)
new_esEs16([], [], cg) → True
new_esEs5(vuu9, vuu110, ty_Bool) → new_esEs19(vuu9, vuu110)
new_esEs4(vuu18, vuu200, ty_Char) → new_esEs8(vuu18, vuu200)
new_esEs21(vuu301, vuu3101, ty_Char) → new_esEs8(vuu301, vuu3101)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs19(False, False) → True
new_esEs21(vuu301, vuu3101, app(app(ty_@2, baf), bag)) → new_esEs7(vuu301, vuu3101, baf, bag)
new_esEs27(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs10(GT, LT) → False
new_esEs10(LT, GT) → False
new_primEqInt(Neg(Succ(vuu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vuu31000))) → False
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(ty_Maybe, he)) → new_esEs12(vuu300, vuu3100, he)
new_esEs22(vuu300, vuu3100, app(ty_Maybe, bcc)) → new_esEs12(vuu300, vuu3100, bcc)
new_esEs26(vuu301, vuu3101, app(ty_Ratio, bge)) → new_esEs11(vuu301, vuu3101, bge)
new_esEs10(EQ, LT) → False
new_esEs10(LT, EQ) → False
new_esEs20(vuu300, vuu3100, app(app(ty_@2, da), db)) → new_esEs7(vuu300, vuu3100, da, db)
new_esEs12(Just(vuu300), Just(vuu3100), app(ty_Maybe, bdg)) → new_esEs12(vuu300, vuu3100, bdg)
new_esEs21(vuu301, vuu3101, ty_Integer) → new_esEs6(vuu301, vuu3101)
new_esEs20(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, app(app(ty_Either, bcg), bch)) → new_esEs15(vuu300, vuu3100, bcg, bch)
new_esEs22(vuu300, vuu3100, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, app(ty_Maybe, ef)) → new_esEs12(vuu9, vuu110, ef)
new_esEs4(vuu18, vuu200, app(ty_[], cf)) → new_esEs16(vuu18, vuu200, cf)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs26(vuu301, vuu3101, app(app(app(ty_@3, bgg), bgh), bha)) → new_esEs14(vuu301, vuu3101, bgg, bgh, bha)
new_esEs12(Just(vuu300), Just(vuu3100), app(app(app(ty_@3, bdh), bea), beb)) → new_esEs14(vuu300, vuu3100, bdh, bea, beb)
new_asAs(True, vuu34) → vuu34
new_esEs27(vuu300, vuu3100, ty_Char) → new_esEs8(vuu300, vuu3100)
new_primMulNat0(Succ(vuu30100), Succ(vuu310100)) → new_primPlusNat0(new_primMulNat0(vuu30100, Succ(vuu310100)), vuu310100)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Int) → new_esEs9(vuu300, vuu3100)
new_primEqInt(Pos(Succ(vuu3000)), Pos(Succ(vuu31000))) → new_primEqNat0(vuu3000, vuu31000)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Ordering, ff) → new_esEs10(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, app(ty_[], fd)) → new_esEs16(vuu9, vuu110, fd)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs26(vuu301, vuu3101, ty_Bool) → new_esEs19(vuu301, vuu3101)
new_esEs5(vuu9, vuu110, app(app(ty_@2, ec), ed)) → new_esEs7(vuu9, vuu110, ec, ed)
new_esEs11(:%(vuu300, vuu301), :%(vuu3100, vuu3101), bdb) → new_asAs(new_esEs24(vuu300, vuu3100, bdb), new_esEs23(vuu301, vuu3101, bdb))
new_esEs25(vuu302, vuu3102, ty_Int) → new_esEs9(vuu302, vuu3102)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs14(vuu300, vuu3100, bcd, bce, bcf)
new_esEs8(Char(vuu300), Char(vuu3100)) → new_primEqNat0(vuu300, vuu3100)
new_primEqNat0(Succ(vuu3000), Succ(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs9(vuu30, vuu310) → new_primEqInt(vuu30, vuu310)
new_esEs25(vuu302, vuu3102, app(app(app(ty_@3, bfe), bff), bfg)) → new_esEs14(vuu302, vuu3102, bfe, bff, bfg)
new_esEs5(vuu9, vuu110, ty_Double) → new_esEs17(vuu9, vuu110)
new_esEs24(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs27(vuu300, vuu3100, app(app(app(ty_@3, caa), cab), cac)) → new_esEs14(vuu300, vuu3100, caa, cab, cac)
new_esEs4(vuu18, vuu200, ty_Int) → new_esEs9(vuu18, vuu200)
new_esEs20(vuu300, vuu3100, ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), app(app(ty_@2, fg), fh), ff) → new_esEs7(vuu300, vuu3100, fg, fh)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Bool, ff) → new_esEs19(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, ty_Char) → new_esEs8(vuu9, vuu110)
new_esEs21(vuu301, vuu3101, app(ty_Ratio, bah)) → new_esEs11(vuu301, vuu3101, bah)
new_esEs21(vuu301, vuu3101, app(ty_[], bbg)) → new_esEs16(vuu301, vuu3101, bbg)
new_esEs27(vuu300, vuu3100, app(app(ty_Either, cad), cae)) → new_esEs15(vuu300, vuu3100, cad, cae)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, app(app(ty_Either, fb), fc)) → new_esEs15(vuu9, vuu110, fb, fc)
new_esEs20(vuu300, vuu3100, app(app(ty_Either, dh), ea)) → new_esEs15(vuu300, vuu3100, dh, ea)
new_esEs27(vuu300, vuu3100, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, app(ty_Ratio, bcb)) → new_esEs11(vuu300, vuu3100, bcb)
new_primEqInt(Pos(Succ(vuu3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(vuu31000))) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs26(vuu301, vuu3101, app(app(ty_Either, bhb), bhc)) → new_esEs15(vuu301, vuu3101, bhb, bhc)
new_esEs21(vuu301, vuu3101, ty_Bool) → new_esEs19(vuu301, vuu3101)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs17(Double(vuu300, vuu301), Double(vuu3100, vuu3101)) → new_esEs9(new_sr(vuu300, vuu3100), new_sr(vuu301, vuu3101))
new_esEs12(Just(vuu300), Just(vuu3100), app(ty_[], bee)) → new_esEs16(vuu300, vuu3100, bee)
new_esEs4(vuu18, vuu200, app(app(ty_@2, be), bf)) → new_esEs7(vuu18, vuu200, be, bf)
The set Q consists of the following terms:
new_esEs12(Just(x0), Just(x1), ty_Char)
new_esEs15(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs15(Left(x0), Left(x1), ty_Int, x2)
new_esEs25(x0, x1, ty_@0)
new_esEs13(@0, @0)
new_primPlusNat1(Zero, Succ(x0))
new_esEs15(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs12(Just(x0), Just(x1), ty_Integer)
new_esEs27(x0, x1, ty_Bool)
new_esEs20(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs25(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, ty_Char)
new_esEs12(Just(x0), Just(x1), app(ty_[], x2))
new_esEs4(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Integer)
new_esEs5(x0, x1, ty_Integer)
new_esEs8(Char(x0), Char(x1))
new_esEs19(False, False)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Char)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs15(Right(x0), Right(x1), x2, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Double)
new_esEs16([], [], x0)
new_esEs12(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs12(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Bool)
new_esEs20(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Integer)
new_esEs15(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(EQ, GT)
new_esEs10(GT, EQ)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(Just(x0), Just(x1), ty_Ordering)
new_esEs20(x0, x1, ty_Float)
new_esEs15(Right(x0), Right(x1), x2, ty_Ordering)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs10(LT, EQ)
new_esEs10(EQ, LT)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Integer)
new_primMulNat0(Zero, Succ(x0))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15(Right(x0), Right(x1), x2, ty_@0)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs15(Left(x0), Right(x1), x2, x3)
new_esEs15(Right(x0), Left(x1), x2, x3)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_@0)
new_esEs10(LT, LT)
new_esEs25(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Integer)
new_esEs15(Right(x0), Right(x1), x2, ty_Integer)
new_esEs25(x0, x1, ty_Ordering)
new_esEs15(Left(x0), Left(x1), ty_Ordering, x2)
new_primPlusNat1(Succ(x0), Zero)
new_esEs15(Left(x0), Left(x1), ty_Float, x2)
new_esEs24(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Int)
new_esEs12(Nothing, Just(x0), x1)
new_esEs12(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs15(Left(x0), Left(x1), ty_@0, x2)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs19(True, True)
new_esEs12(Just(x0), Just(x1), ty_@0)
new_esEs22(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_@0)
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_sr(Neg(x0), Neg(x1))
new_esEs26(x0, x1, ty_Char)
new_esEs15(Left(x0), Left(x1), ty_Bool, x2)
new_primPlusNat0(Succ(x0), x1)
new_esEs22(x0, x1, ty_Bool)
new_esEs15(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs5(x0, x1, ty_Float)
new_esEs15(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs15(Right(x0), Right(x1), x2, ty_Char)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_Float)
new_primEqNat0(Zero, Zero)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs16(:(x0, x1), :(x2, x3), x4)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs18(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Integer)
new_esEs12(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat0(Zero, x0)
new_esEs10(GT, GT)
new_sr(Pos(x0), Pos(x1))
new_esEs6(Integer(x0), Integer(x1))
new_esEs15(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs15(Right(x0), Right(x1), x2, ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs16(:(x0, x1), [], x2)
new_esEs15(Right(x0), Right(x1), x2, ty_Int)
new_primMulNat0(Zero, Zero)
new_esEs5(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Char)
new_esEs15(Left(x0), Left(x1), ty_Char, x2)
new_esEs22(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(x0, x1)
new_esEs12(Just(x0), Nothing, x1)
new_esEs25(x0, x1, ty_Bool)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs12(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_esEs21(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(Just(x0), Just(x1), ty_Bool)
new_esEs10(LT, GT)
new_esEs10(GT, LT)
new_primMulNat0(Succ(x0), Zero)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16([], :(x0, x1), x2)
new_esEs27(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_Double)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs12(Nothing, Nothing, x0)
new_esEs17(Double(x0, x1), Double(x2, x3))
new_esEs15(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs12(Just(x0), Just(x1), ty_Double)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_@0)
new_esEs11(:%(x0, x1), :%(x2, x3), x4)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Int)
new_esEs14(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs22(x0, x1, ty_Int)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Succ(x0), Zero)
new_esEs5(x0, x1, ty_Bool)
new_esEs15(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, ty_Bool)
new_esEs15(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs19(True, False)
new_esEs19(False, True)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs15(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Bool)
new_esEs15(Left(x0), Left(x1), ty_Integer, x2)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Zero)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Float)
new_esEs15(Right(x0), Right(x1), x2, ty_Float)
new_esEs27(x0, x1, ty_Int)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(False, x0)
new_esEs22(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Double)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs15(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs10(EQ, EQ)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs26(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Double)
new_esEs7(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs21(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Ordering)
new_esEs12(Just(x0), Just(x1), ty_Float)
new_asAs(True, x0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Bool)
new_esEs20(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Ordering)
new_esEs15(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs12(Just(x0), Just(x1), ty_Int)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Ys(vuu9, :(vuu110, vuu111), bd) → new_span2Ys1(vuu9, vuu110, vuu111, new_esEs5(vuu9, vuu110, bd), bd)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 3 >= 5
- new_span2Zs(vuu18, :(vuu200, vuu201), bb) → new_span2Zs1(vuu18, vuu200, vuu201, new_esEs4(vuu18, vuu200, bb), bb)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 3 >= 5
- new_span2Ys1(vuu40, vuu41, vuu42, True, ba) → new_span2Ys(vuu40, vuu42, ba)
The graph contains the following edges 1 >= 1, 3 >= 2, 5 >= 3
- new_span2Ys1(vuu40, vuu41, vuu42, True, ba) → new_span2Zs(vuu40, vuu42, ba)
The graph contains the following edges 1 >= 1, 3 >= 2, 5 >= 3
- new_span2Zs1(vuu49, vuu50, vuu51, True, bc) → new_span2Ys(vuu49, vuu51, bc)
The graph contains the following edges 1 >= 1, 3 >= 2, 5 >= 3
- new_span2Zs1(vuu49, vuu50, vuu51, True, bc) → new_span2Zs(vuu49, vuu51, bc)
The graph contains the following edges 1 >= 1, 3 >= 2, 5 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_groupBy(:(vuu30, vuu31), ba) → new_groupBy(new_groupByZs0(vuu30, vuu31, ba), ba)
The TRS R consists of the following rules:
new_esEs4(vuu18, vuu200, app(app(app(ty_@3, bg), bh), ca)) → new_esEs14(vuu18, vuu200, bg, bh, ca)
new_esEs21(vuu301, vuu3101, ty_@0) → new_esEs13(vuu301, vuu3101)
new_esEs22(vuu300, vuu3100, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs19(True, False) → False
new_esEs19(False, True) → False
new_esEs5(vuu9, vuu110, app(ty_Ratio, da)) → new_esEs11(vuu9, vuu110, da)
new_esEs27(vuu300, vuu3100, app(ty_[], cag)) → new_esEs16(vuu300, vuu3100, cag)
new_primPlusNat1(Succ(vuu5700), Succ(vuu3101000)) → Succ(Succ(new_primPlusNat1(vuu5700, vuu3101000)))
new_esEs21(vuu301, vuu3101, ty_Double) → new_esEs17(vuu301, vuu3101)
new_esEs25(vuu302, vuu3102, app(ty_[], bgc)) → new_esEs16(vuu302, vuu3102, bgc)
new_primEqInt(Neg(Succ(vuu3000)), Pos(vuu3100)) → False
new_primEqInt(Pos(Succ(vuu3000)), Neg(vuu3100)) → False
new_esEs25(vuu302, vuu3102, ty_Bool) → new_esEs19(vuu302, vuu3102)
new_esEs25(vuu302, vuu3102, ty_Char) → new_esEs8(vuu302, vuu3102)
new_esEs25(vuu302, vuu3102, app(ty_Ratio, bfd)) → new_esEs11(vuu302, vuu3102, bfd)
new_esEs25(vuu302, vuu3102, ty_@0) → new_esEs13(vuu302, vuu3102)
new_esEs15(Left(vuu300), Right(vuu3100), ha, ff) → False
new_esEs15(Right(vuu300), Left(vuu3100), ha, ff) → False
new_esEs18(Float(vuu300, vuu301), Float(vuu3100, vuu3101)) → new_esEs9(new_sr(vuu300, vuu3100), new_sr(vuu301, vuu3101))
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(app(ty_Either, baa), bab)) → new_esEs15(vuu300, vuu3100, baa, bab)
new_esEs26(vuu301, vuu3101, ty_Int) → new_esEs9(vuu301, vuu3101)
new_esEs27(vuu300, vuu3100, app(ty_Ratio, bhh)) → new_esEs11(vuu300, vuu3100, bhh)
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(ty_Ratio, hd)) → new_esEs11(vuu300, vuu3100, hd)
new_primEqInt(Neg(Zero), Pos(Succ(vuu31000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vuu31000))) → False
new_esEs13(@0, @0) → True
new_span2Ys10(vuu40, vuu41, vuu42, False, fd) → []
new_esEs12(Just(vuu300), Just(vuu3100), app(app(ty_@2, bae), baf)) → new_esEs7(vuu300, vuu3100, bae, baf)
new_esEs27(vuu300, vuu3100, app(app(ty_@2, bhf), bhg)) → new_esEs7(vuu300, vuu3100, bhf, bhg)
new_esEs20(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), app(app(ty_Either, gf), gg), ff) → new_esEs15(vuu300, vuu3100, gf, gg)
new_esEs22(vuu300, vuu3100, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs26(vuu301, vuu3101, app(ty_Maybe, bgg)) → new_esEs12(vuu301, vuu3101, bgg)
new_esEs22(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_primMulNat0(Zero, Zero) → Zero
new_esEs28(vuu30, vuu310, ty_Bool) → new_esEs19(vuu30, vuu310)
new_esEs28(vuu30, vuu310, ty_Ordering) → new_esEs10(vuu30, vuu310)
new_esEs22(vuu300, vuu3100, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs21(vuu301, vuu3101, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs14(vuu301, vuu3101, bdb, bdc, bdd)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Float, ff) → new_esEs18(vuu300, vuu3100)
new_esEs7(@2(vuu300, vuu301), @2(vuu3100, vuu3101), bbh, bca) → new_asAs(new_esEs22(vuu300, vuu3100, bbh), new_esEs21(vuu301, vuu3101, bca))
new_esEs26(vuu301, vuu3101, app(ty_[], bhe)) → new_esEs16(vuu301, vuu3101, bhe)
new_esEs21(vuu301, vuu3101, app(app(ty_Either, bde), bdf)) → new_esEs15(vuu301, vuu3101, bde, bdf)
new_esEs28(vuu30, vuu310, app(ty_[], ea)) → new_esEs16(vuu30, vuu310, ea)
new_primPlusNat0(Zero, vuu310100) → Succ(vuu310100)
new_esEs4(vuu18, vuu200, ty_Ordering) → new_esEs10(vuu18, vuu200)
new_esEs6(Integer(vuu300), Integer(vuu3100)) → new_primEqInt(vuu300, vuu3100)
new_esEs4(vuu18, vuu200, app(ty_Ratio, be)) → new_esEs11(vuu18, vuu200, be)
new_esEs28(vuu30, vuu310, ty_Integer) → new_esEs6(vuu30, vuu310)
new_esEs5(vuu9, vuu110, app(app(app(ty_@3, dc), dd), de)) → new_esEs14(vuu9, vuu110, dc, dd, de)
new_esEs25(vuu302, vuu3102, ty_Float) → new_esEs18(vuu302, vuu3102)
new_esEs16(:(vuu300, vuu301), :(vuu3100, vuu3101), ea) → new_asAs(new_esEs20(vuu300, vuu3100, ea), new_esEs16(vuu301, vuu3101, ea))
new_esEs26(vuu301, vuu3101, ty_Ordering) → new_esEs10(vuu301, vuu3101)
new_sr(Neg(vuu3010), Pos(vuu31010)) → Neg(new_primMulNat0(vuu3010, vuu31010))
new_sr(Pos(vuu3010), Neg(vuu31010)) → Neg(new_primMulNat0(vuu3010, vuu31010))
new_esEs15(Left(vuu300), Left(vuu3100), ty_Char, ff) → new_esEs8(vuu300, vuu3100)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs25(vuu302, vuu3102, app(app(ty_Either, bga), bgb)) → new_esEs15(vuu302, vuu3102, bga, bgb)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Int, ff) → new_esEs9(vuu300, vuu3100)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, ty_Integer) → new_esEs6(vuu9, vuu110)
new_esEs12(Just(vuu300), Just(vuu3100), ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, app(ty_Ratio, ed)) → new_esEs11(vuu300, vuu3100, ed)
new_esEs12(Just(vuu300), Just(vuu3100), app(app(ty_Either, bbd), bbe)) → new_esEs15(vuu300, vuu3100, bbd, bbe)
new_esEs22(vuu300, vuu3100, app(ty_[], bfa)) → new_esEs16(vuu300, vuu3100, bfa)
new_groupByZs00(vuu18, vuu19, vuu20, False, bb) → :(vuu19, vuu20)
new_esEs26(vuu301, vuu3101, ty_Float) → new_esEs18(vuu301, vuu3101)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs14(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), bcc, bcd, bce) → new_asAs(new_esEs27(vuu300, vuu3100, bcc), new_asAs(new_esEs26(vuu301, vuu3101, bcd), new_esEs25(vuu302, vuu3102, bce)))
new_esEs26(vuu301, vuu3101, ty_Integer) → new_esEs6(vuu301, vuu3101)
new_esEs4(vuu18, vuu200, app(app(ty_Either, cb), cc)) → new_esEs15(vuu18, vuu200, cb, cc)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Double, ff) → new_esEs17(vuu300, vuu3100)
new_primEqNat0(Zero, Succ(vuu31000)) → False
new_primEqNat0(Succ(vuu3000), Zero) → False
new_esEs21(vuu301, vuu3101, ty_Int) → new_esEs9(vuu301, vuu3101)
new_esEs26(vuu301, vuu3101, app(app(ty_@2, bgd), bge)) → new_esEs7(vuu301, vuu3101, bgd, bge)
new_groupByZs0(vuu30, :(vuu310, vuu311), ba) → new_groupByZs00(vuu30, vuu310, vuu311, new_esEs28(vuu30, vuu310, ba), ba)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs4(vuu18, vuu200, ty_Float) → new_esEs18(vuu18, vuu200)
new_esEs25(vuu302, vuu3102, app(app(ty_@2, bfb), bfc)) → new_esEs7(vuu302, vuu3102, bfb, bfc)
new_esEs4(vuu18, vuu200, ty_Bool) → new_esEs19(vuu18, vuu200)
new_esEs23(vuu301, vuu3101, ty_Integer) → new_esEs6(vuu301, vuu3101)
new_esEs22(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs21(vuu301, vuu3101, app(ty_Maybe, bda)) → new_esEs12(vuu301, vuu3101, bda)
new_esEs16([], :(vuu3100, vuu3101), ea) → False
new_esEs16(:(vuu300, vuu301), [], ea) → False
new_esEs28(vuu30, vuu310, ty_Float) → new_esEs18(vuu30, vuu310)
new_span2Zs0(vuu18, [], bb) → []
new_esEs5(vuu9, vuu110, ty_Ordering) → new_esEs10(vuu9, vuu110)
new_esEs5(vuu9, vuu110, ty_Float) → new_esEs18(vuu9, vuu110)
new_esEs28(vuu30, vuu310, ty_@0) → new_esEs13(vuu30, vuu310)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs26(vuu301, vuu3101, ty_@0) → new_esEs13(vuu301, vuu3101)
new_esEs15(Left(vuu300), Left(vuu3100), app(ty_[], gh), ff) → new_esEs16(vuu300, vuu3100, gh)
new_esEs24(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_esEs27(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs25(vuu302, vuu3102, ty_Integer) → new_esEs6(vuu302, vuu3102)
new_esEs26(vuu301, vuu3101, ty_Char) → new_esEs8(vuu301, vuu3101)
new_span2Zs11(vuu49, vuu50, vuu51, vuu56, vuu55, bbg) → vuu55
new_esEs21(vuu301, vuu3101, ty_Float) → new_esEs18(vuu301, vuu3101)
new_esEs4(vuu18, vuu200, ty_@0) → new_esEs13(vuu18, vuu200)
new_esEs26(vuu301, vuu3101, ty_Double) → new_esEs17(vuu301, vuu3101)
new_esEs4(vuu18, vuu200, ty_Integer) → new_esEs6(vuu18, vuu200)
new_span2Ys11(vuu40, vuu41, vuu42, vuu54, vuu53, fd) → :(vuu41, vuu54)
new_groupByZs0(vuu30, [], ba) → []
new_groupByZs00(vuu18, vuu19, vuu20, True, bb) → new_span2Zs0(vuu18, vuu20, bb)
new_esEs12(Just(vuu300), Just(vuu3100), app(ty_Ratio, bag)) → new_esEs11(vuu300, vuu3100, bag)
new_esEs22(vuu300, vuu3100, ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs25(vuu302, vuu3102, ty_Double) → new_esEs17(vuu302, vuu3102)
new_sr(Neg(vuu3010), Neg(vuu31010)) → Pos(new_primMulNat0(vuu3010, vuu31010))
new_esEs10(LT, LT) → True
new_esEs10(EQ, GT) → False
new_esEs10(GT, EQ) → False
new_esEs27(vuu300, vuu3100, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, app(ty_[], fc)) → new_esEs16(vuu300, vuu3100, fc)
new_esEs12(Just(vuu300), Nothing, bad) → False
new_esEs12(Nothing, Just(vuu3100), bad) → False
new_sr(Pos(vuu3010), Pos(vuu31010)) → Pos(new_primMulNat0(vuu3010, vuu31010))
new_asAs(False, vuu34) → False
new_esEs27(vuu300, vuu3100, app(ty_Maybe, caa)) → new_esEs12(vuu300, vuu3100, caa)
new_primEqNat0(Zero, Zero) → True
new_esEs20(vuu300, vuu3100, app(ty_Maybe, ee)) → new_esEs12(vuu300, vuu3100, ee)
new_primMulNat0(Zero, Succ(vuu310100)) → Zero
new_primMulNat0(Succ(vuu30100), Zero) → Zero
new_esEs15(Left(vuu300), Left(vuu3100), app(app(app(ty_@3, gc), gd), ge), ff) → new_esEs14(vuu300, vuu3100, gc, gd, ge)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Integer, ff) → new_esEs6(vuu300, vuu3100)
new_span2Zs10(vuu49, vuu50, vuu51, False, bbg) → :(vuu50, vuu51)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), app(ty_Maybe, gb), ff) → new_esEs12(vuu300, vuu3100, gb)
new_esEs10(GT, GT) → True
new_esEs25(vuu302, vuu3102, ty_Ordering) → new_esEs10(vuu302, vuu3102)
new_esEs4(vuu18, vuu200, app(ty_Maybe, bf)) → new_esEs12(vuu18, vuu200, bf)
new_esEs23(vuu301, vuu3101, ty_Int) → new_esEs9(vuu301, vuu3101)
new_esEs22(vuu300, vuu3100, app(app(ty_@2, bdh), bea)) → new_esEs7(vuu300, vuu3100, bdh, bea)
new_esEs12(Nothing, Nothing, bad) → True
new_esEs19(True, True) → True
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(ty_[], bac)) → new_esEs16(vuu300, vuu3100, bac)
new_esEs27(vuu300, vuu3100, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs27(vuu300, vuu3100, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(app(app(ty_@3, hf), hg), hh)) → new_esEs14(vuu300, vuu3100, hf, hg, hh)
new_esEs5(vuu9, vuu110, ty_@0) → new_esEs13(vuu9, vuu110)
new_primPlusNat0(Succ(vuu570), vuu310100) → Succ(Succ(new_primPlusNat1(vuu570, vuu310100)))
new_esEs5(vuu9, vuu110, ty_Int) → new_esEs9(vuu9, vuu110)
new_esEs20(vuu300, vuu3100, app(app(app(ty_@3, ef), eg), eh)) → new_esEs14(vuu300, vuu3100, ef, eg, eh)
new_esEs25(vuu302, vuu3102, app(ty_Maybe, bfe)) → new_esEs12(vuu302, vuu3102, bfe)
new_esEs15(Left(vuu300), Left(vuu3100), app(ty_Ratio, ga), ff) → new_esEs11(vuu300, vuu3100, ga)
new_esEs28(vuu30, vuu310, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs14(vuu30, vuu310, bcc, bcd, bce)
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(app(ty_@2, hb), hc)) → new_esEs7(vuu300, vuu3100, hb, hc)
new_esEs15(Left(vuu300), Left(vuu3100), ty_@0, ff) → new_esEs13(vuu300, vuu3100)
new_primEqInt(Neg(Succ(vuu3000)), Neg(Succ(vuu31000))) → new_primEqNat0(vuu3000, vuu31000)
new_esEs10(EQ, EQ) → True
new_esEs4(vuu18, vuu200, ty_Double) → new_esEs17(vuu18, vuu200)
new_esEs27(vuu300, vuu3100, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs21(vuu301, vuu3101, ty_Ordering) → new_esEs10(vuu301, vuu3101)
new_primPlusNat1(Zero, Succ(vuu3101000)) → Succ(vuu3101000)
new_primPlusNat1(Succ(vuu5700), Zero) → Succ(vuu5700)
new_esEs16([], [], ea) → True
new_esEs28(vuu30, vuu310, app(app(ty_Either, ha), ff)) → new_esEs15(vuu30, vuu310, ha, ff)
new_esEs5(vuu9, vuu110, ty_Bool) → new_esEs19(vuu9, vuu110)
new_esEs4(vuu18, vuu200, ty_Char) → new_esEs8(vuu18, vuu200)
new_esEs21(vuu301, vuu3101, ty_Char) → new_esEs8(vuu301, vuu3101)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_span2Ys0(vuu9, [], ce) → []
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs19(False, False) → True
new_esEs21(vuu301, vuu3101, app(app(ty_@2, bcf), bcg)) → new_esEs7(vuu301, vuu3101, bcf, bcg)
new_esEs28(vuu30, vuu310, ty_Int) → new_esEs9(vuu30, vuu310)
new_esEs27(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs10(LT, GT) → False
new_esEs10(GT, LT) → False
new_primEqInt(Neg(Zero), Neg(Succ(vuu31000))) → False
new_primEqInt(Neg(Succ(vuu3000)), Neg(Zero)) → False
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(ty_Maybe, he)) → new_esEs12(vuu300, vuu3100, he)
new_esEs22(vuu300, vuu3100, app(ty_Maybe, bec)) → new_esEs12(vuu300, vuu3100, bec)
new_esEs28(vuu30, vuu310, app(ty_Ratio, bcb)) → new_esEs11(vuu30, vuu310, bcb)
new_span2Ys10(vuu40, vuu41, vuu42, True, fd) → new_span2Ys11(vuu40, vuu41, vuu42, new_span2Ys0(vuu40, vuu42, fd), new_span2Zs0(vuu40, vuu42, fd), fd)
new_esEs26(vuu301, vuu3101, app(ty_Ratio, bgf)) → new_esEs11(vuu301, vuu3101, bgf)
new_esEs10(LT, EQ) → False
new_esEs10(EQ, LT) → False
new_esEs20(vuu300, vuu3100, app(app(ty_@2, eb), ec)) → new_esEs7(vuu300, vuu3100, eb, ec)
new_esEs21(vuu301, vuu3101, ty_Integer) → new_esEs6(vuu301, vuu3101)
new_esEs28(vuu30, vuu310, ty_Double) → new_esEs17(vuu30, vuu310)
new_esEs12(Just(vuu300), Just(vuu3100), app(ty_Maybe, bah)) → new_esEs12(vuu300, vuu3100, bah)
new_esEs20(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, app(app(ty_Either, beg), beh)) → new_esEs15(vuu300, vuu3100, beg, beh)
new_esEs5(vuu9, vuu110, app(ty_Maybe, db)) → new_esEs12(vuu9, vuu110, db)
new_esEs4(vuu18, vuu200, app(ty_[], cd)) → new_esEs16(vuu18, vuu200, cd)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs26(vuu301, vuu3101, app(app(app(ty_@3, bgh), bha), bhb)) → new_esEs14(vuu301, vuu3101, bgh, bha, bhb)
new_esEs12(Just(vuu300), Just(vuu3100), app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs14(vuu300, vuu3100, bba, bbb, bbc)
new_span2Ys0(vuu9, :(vuu110, vuu111), ce) → new_span2Ys10(vuu9, vuu110, vuu111, new_esEs5(vuu9, vuu110, ce), ce)
new_asAs(True, vuu34) → vuu34
new_esEs27(vuu300, vuu3100, ty_Char) → new_esEs8(vuu300, vuu3100)
new_primMulNat0(Succ(vuu30100), Succ(vuu310100)) → new_primPlusNat0(new_primMulNat0(vuu30100, Succ(vuu310100)), vuu310100)
new_esEs28(vuu30, vuu310, app(app(ty_@2, bbh), bca)) → new_esEs7(vuu30, vuu310, bbh, bca)
new_esEs28(vuu30, vuu310, app(ty_Maybe, bad)) → new_esEs12(vuu30, vuu310, bad)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Int) → new_esEs9(vuu300, vuu3100)
new_primEqInt(Pos(Succ(vuu3000)), Pos(Succ(vuu31000))) → new_primEqNat0(vuu3000, vuu31000)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Ordering, ff) → new_esEs10(vuu300, vuu3100)
new_span2Zs0(vuu18, :(vuu200, vuu201), bb) → new_span2Zs10(vuu18, vuu200, vuu201, new_esEs4(vuu18, vuu200, bb), bb)
new_esEs22(vuu300, vuu3100, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, app(ty_[], dh)) → new_esEs16(vuu9, vuu110, dh)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs26(vuu301, vuu3101, ty_Bool) → new_esEs19(vuu301, vuu3101)
new_esEs5(vuu9, vuu110, app(app(ty_@2, cf), cg)) → new_esEs7(vuu9, vuu110, cf, cg)
new_esEs11(:%(vuu300, vuu301), :%(vuu3100, vuu3101), bcb) → new_asAs(new_esEs24(vuu300, vuu3100, bcb), new_esEs23(vuu301, vuu3101, bcb))
new_esEs25(vuu302, vuu3102, ty_Int) → new_esEs9(vuu302, vuu3102)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, app(app(app(ty_@3, bed), bee), bef)) → new_esEs14(vuu300, vuu3100, bed, bee, bef)
new_esEs8(Char(vuu300), Char(vuu3100)) → new_primEqNat0(vuu300, vuu3100)
new_primEqNat0(Succ(vuu3000), Succ(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs9(vuu30, vuu310) → new_primEqInt(vuu30, vuu310)
new_esEs25(vuu302, vuu3102, app(app(app(ty_@3, bff), bfg), bfh)) → new_esEs14(vuu302, vuu3102, bff, bfg, bfh)
new_esEs5(vuu9, vuu110, ty_Double) → new_esEs17(vuu9, vuu110)
new_esEs28(vuu30, vuu310, ty_Char) → new_esEs8(vuu30, vuu310)
new_esEs24(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs27(vuu300, vuu3100, app(app(app(ty_@3, cab), cac), cad)) → new_esEs14(vuu300, vuu3100, cab, cac, cad)
new_esEs4(vuu18, vuu200, ty_Int) → new_esEs9(vuu18, vuu200)
new_esEs20(vuu300, vuu3100, ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), app(app(ty_@2, fg), fh), ff) → new_esEs7(vuu300, vuu3100, fg, fh)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Bool, ff) → new_esEs19(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, ty_Char) → new_esEs8(vuu9, vuu110)
new_esEs21(vuu301, vuu3101, app(ty_Ratio, bch)) → new_esEs11(vuu301, vuu3101, bch)
new_esEs21(vuu301, vuu3101, app(ty_[], bdg)) → new_esEs16(vuu301, vuu3101, bdg)
new_esEs27(vuu300, vuu3100, app(app(ty_Either, cae), caf)) → new_esEs15(vuu300, vuu3100, cae, caf)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_span2Zs10(vuu49, vuu50, vuu51, True, bbg) → new_span2Zs11(vuu49, vuu50, vuu51, new_span2Ys0(vuu49, vuu51, bbg), new_span2Zs0(vuu49, vuu51, bbg), bbg)
new_esEs20(vuu300, vuu3100, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, app(app(ty_Either, df), dg)) → new_esEs15(vuu9, vuu110, df, dg)
new_esEs20(vuu300, vuu3100, app(app(ty_Either, fa), fb)) → new_esEs15(vuu300, vuu3100, fa, fb)
new_esEs27(vuu300, vuu3100, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, app(ty_Ratio, beb)) → new_esEs11(vuu300, vuu3100, beb)
new_primEqInt(Pos(Zero), Pos(Succ(vuu31000))) → False
new_primEqInt(Pos(Succ(vuu3000)), Pos(Zero)) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs26(vuu301, vuu3101, app(app(ty_Either, bhc), bhd)) → new_esEs15(vuu301, vuu3101, bhc, bhd)
new_esEs21(vuu301, vuu3101, ty_Bool) → new_esEs19(vuu301, vuu3101)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs17(Double(vuu300, vuu301), Double(vuu3100, vuu3101)) → new_esEs9(new_sr(vuu300, vuu3100), new_sr(vuu301, vuu3101))
new_esEs12(Just(vuu300), Just(vuu3100), app(ty_[], bbf)) → new_esEs16(vuu300, vuu3100, bbf)
new_esEs4(vuu18, vuu200, app(app(ty_@2, bc), bd)) → new_esEs7(vuu18, vuu200, bc, bd)
The set Q consists of the following terms:
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Just(x0), Just(x1), ty_Char)
new_esEs15(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs15(Left(x0), Left(x1), ty_Int, x2)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_@0)
new_esEs13(@0, @0)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(Just(x0), Just(x1), app(ty_[], x2))
new_primPlusNat1(Zero, Succ(x0))
new_esEs15(Left(x0), Left(x1), app(ty_[], x2), x3)
new_span2Zs11(x0, x1, x2, x3, x4, x5)
new_esEs12(Just(x0), Just(x1), ty_Integer)
new_esEs28(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Bool)
new_esEs28(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs25(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs28(x0, x1, ty_Int)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Char)
new_groupByZs0(x0, [], x1)
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Integer)
new_esEs5(x0, x1, ty_Integer)
new_esEs8(Char(x0), Char(x1))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(False, False)
new_esEs22(x0, x1, ty_Char)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs15(Right(x0), Right(x1), x2, ty_Bool)
new_esEs12(Nothing, Just(x0), x1)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primEqInt(Neg(Zero), Neg(Zero))
new_groupByZs00(x0, x1, x2, True, x3)
new_esEs12(Just(x0), Nothing, x1)
new_esEs28(x0, x1, ty_Bool)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs12(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Double)
new_span2Zs10(x0, x1, x2, False, x3)
new_esEs4(x0, x1, ty_Bool)
new_esEs20(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Integer)
new_esEs15(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs12(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs10(GT, EQ)
new_esEs10(EQ, GT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(Just(x0), Just(x1), ty_Ordering)
new_esEs11(:%(x0, x1), :%(x2, x3), x4)
new_esEs20(x0, x1, ty_Float)
new_esEs15(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(EQ, LT)
new_esEs10(LT, EQ)
new_esEs28(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_span2Zs0(x0, [], x1)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Integer)
new_primMulNat0(Zero, Succ(x0))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs15(Right(x0), Right(x1), x2, ty_@0)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs15(Left(x0), Right(x1), x2, x3)
new_esEs15(Right(x0), Left(x1), x2, x3)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_@0)
new_esEs10(LT, LT)
new_esEs25(x0, x1, ty_Integer)
new_esEs5(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Integer)
new_esEs15(Right(x0), Right(x1), x2, ty_Integer)
new_esEs25(x0, x1, ty_Ordering)
new_esEs15(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs26(x0, x1, app(ty_[], x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs15(Left(x0), Left(x1), ty_Float, x2)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Int)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs15(Left(x0), Left(x1), ty_@0, x2)
new_esEs16([], :(x0, x1), x2)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs19(True, True)
new_esEs12(Just(x0), Just(x1), ty_@0)
new_groupByZs00(x0, x1, x2, False, x3)
new_esEs22(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_@0)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_@0)
new_esEs15(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_sr(Neg(x0), Neg(x1))
new_esEs26(x0, x1, ty_Char)
new_esEs15(Left(x0), Left(x1), ty_Bool, x2)
new_primPlusNat0(Succ(x0), x1)
new_esEs28(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_Bool)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs15(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs5(x0, x1, ty_Float)
new_esEs15(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs15(Right(x0), Right(x1), x2, ty_Char)
new_esEs4(x0, x1, ty_Float)
new_primEqNat0(Zero, Zero)
new_primEqNat0(Zero, Succ(x0))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs12(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Int)
new_esEs18(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Integer)
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_esEs10(GT, GT)
new_sr(Pos(x0), Pos(x1))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs6(Integer(x0), Integer(x1))
new_esEs15(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs15(Right(x0), Right(x1), x2, ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs15(Right(x0), Right(x1), x2, ty_Int)
new_primMulNat0(Zero, Zero)
new_esEs5(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(:(x0, x1), :(x2, x3), x4)
new_esEs28(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Char)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Ordering)
new_esEs15(Left(x0), Left(x1), ty_Char, x2)
new_esEs12(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(x0, x1)
new_esEs25(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Float)
new_span2Ys0(x0, [], x1)
new_esEs16(:(x0, x1), [], x2)
new_esEs21(x0, x1, ty_Char)
new_esEs12(Just(x0), Just(x1), ty_Bool)
new_span2Ys0(x0, :(x1, x2), x3)
new_esEs10(GT, LT)
new_esEs10(LT, GT)
new_primMulNat0(Succ(x0), Zero)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Double)
new_esEs17(Double(x0, x1), Double(x2, x3))
new_esEs15(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs12(Just(x0), Just(x1), ty_Double)
new_esEs16([], [], x0)
new_esEs28(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_@0)
new_span2Ys10(x0, x1, x2, True, x3)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Int)
new_esEs14(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Int)
new_esEs28(x0, x1, ty_Float)
new_span2Ys11(x0, x1, x2, x3, x4, x5)
new_primEqNat0(Succ(x0), Zero)
new_esEs5(x0, x1, ty_Bool)
new_esEs15(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, ty_Bool)
new_esEs15(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_span2Zs10(x0, x1, x2, True, x3)
new_span2Zs0(x0, :(x1, x2), x3)
new_esEs19(False, True)
new_esEs19(True, False)
new_esEs15(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Bool)
new_esEs15(Left(x0), Left(x1), ty_Integer, x2)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Zero, Zero)
new_esEs5(x0, x1, ty_Double)
new_esEs15(Right(x0), Right(x1), x2, ty_Float)
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Int)
new_asAs(False, x0)
new_esEs22(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Double)
new_esEs15(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs10(EQ, EQ)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs26(x0, x1, ty_Double)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Ordering)
new_esEs12(Just(x0), Just(x1), ty_Float)
new_asAs(True, x0)
new_span2Ys10(x0, x1, x2, False, x3)
new_esEs7(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Bool)
new_esEs20(x0, x1, ty_Ordering)
new_groupByZs0(x0, :(x1, x2), x3)
new_esEs5(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Char)
new_esEs12(Nothing, Nothing, x0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs15(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs12(Just(x0), Just(x1), ty_Int)
new_esEs20(x0, x1, ty_Double)
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_groupBy(:(vuu30, vuu31), ba) → new_groupBy(new_groupByZs0(vuu30, vuu31, ba), ba)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:
POL(:(x1, x2)) = 1 + x2
POL(:%(x1, x2)) = 0
POL(@0) = 0
POL(@2(x1, x2)) = 0
POL(@3(x1, x2, x3)) = 0
POL(Char(x1)) = 0
POL(Double(x1, x2)) = 0
POL(EQ) = 0
POL(False) = 0
POL(Float(x1, x2)) = 0
POL(GT) = 0
POL(Integer(x1)) = 0
POL(Just(x1)) = 0
POL(LT) = 0
POL(Left(x1)) = 0
POL(Neg(x1)) = 0
POL(Nothing) = 0
POL(Pos(x1)) = 0
POL(Right(x1)) = 0
POL(Succ(x1)) = 0
POL(True) = 0
POL(Zero) = 0
POL([]) = 0
POL(app(x1, x2)) = x2
POL(new_asAs(x1, x2)) = 0
POL(new_esEs10(x1, x2)) = 0
POL(new_esEs11(x1, x2, x3)) = 0
POL(new_esEs12(x1, x2, x3)) = 0
POL(new_esEs13(x1, x2)) = 0
POL(new_esEs14(x1, x2, x3, x4, x5)) = x1
POL(new_esEs15(x1, x2, x3, x4)) = 0
POL(new_esEs16(x1, x2, x3)) = 0
POL(new_esEs17(x1, x2)) = 0
POL(new_esEs18(x1, x2)) = 0
POL(new_esEs19(x1, x2)) = 0
POL(new_esEs20(x1, x2, x3)) = 1 + x1 + x2
POL(new_esEs21(x1, x2, x3)) = 0
POL(new_esEs22(x1, x2, x3)) = 1 + x1 + x2
POL(new_esEs23(x1, x2, x3)) = 0
POL(new_esEs24(x1, x2, x3)) = x1
POL(new_esEs25(x1, x2, x3)) = 0
POL(new_esEs26(x1, x2, x3)) = 0
POL(new_esEs27(x1, x2, x3)) = x1 + x3
POL(new_esEs28(x1, x2, x3)) = x1
POL(new_esEs4(x1, x2, x3)) = 1 + x1 + x3
POL(new_esEs5(x1, x2, x3)) = 0
POL(new_esEs6(x1, x2)) = x1
POL(new_esEs7(x1, x2, x3, x4)) = 0
POL(new_esEs8(x1, x2)) = 0
POL(new_esEs9(x1, x2)) = 0
POL(new_groupBy(x1, x2)) = x1
POL(new_groupByZs0(x1, x2, x3)) = x2
POL(new_groupByZs00(x1, x2, x3, x4, x5)) = 1 + x3
POL(new_primEqInt(x1, x2)) = 0
POL(new_primEqNat0(x1, x2)) = 0
POL(new_primMulNat0(x1, x2)) = 0
POL(new_primPlusNat0(x1, x2)) = 0
POL(new_primPlusNat1(x1, x2)) = 0
POL(new_span2Ys0(x1, x2, x3)) = x2
POL(new_span2Ys10(x1, x2, x3, x4, x5)) = 1 + x3
POL(new_span2Ys11(x1, x2, x3, x4, x5, x6)) = 1 + x4
POL(new_span2Zs0(x1, x2, x3)) = x2
POL(new_span2Zs10(x1, x2, x3, x4, x5)) = 1 + x3
POL(new_span2Zs11(x1, x2, x3, x4, x5, x6)) = x5
POL(new_sr(x1, x2)) = 0
POL(ty_@0) = 0
POL(ty_@2) = 0
POL(ty_@3) = 0
POL(ty_Bool) = 1
POL(ty_Char) = 1
POL(ty_Double) = 0
POL(ty_Either) = 0
POL(ty_Float) = 1
POL(ty_Int) = 0
POL(ty_Integer) = 0
POL(ty_Maybe) = 0
POL(ty_Ordering) = 0
POL(ty_Ratio) = 0
POL(ty_[]) = 0
The following usable rules [17] were oriented:
new_span2Zs0(vuu18, [], bb) → []
new_span2Zs10(vuu49, vuu50, vuu51, False, bbg) → :(vuu50, vuu51)
new_span2Ys10(vuu40, vuu41, vuu42, False, fd) → []
new_span2Zs11(vuu49, vuu50, vuu51, vuu56, vuu55, bbg) → vuu55
new_span2Zs0(vuu18, :(vuu200, vuu201), bb) → new_span2Zs10(vuu18, vuu200, vuu201, new_esEs4(vuu18, vuu200, bb), bb)
new_groupByZs0(vuu30, [], ba) → []
new_span2Ys11(vuu40, vuu41, vuu42, vuu54, vuu53, fd) → :(vuu41, vuu54)
new_groupByZs00(vuu18, vuu19, vuu20, False, bb) → :(vuu19, vuu20)
new_span2Ys10(vuu40, vuu41, vuu42, True, fd) → new_span2Ys11(vuu40, vuu41, vuu42, new_span2Ys0(vuu40, vuu42, fd), new_span2Zs0(vuu40, vuu42, fd), fd)
new_span2Zs10(vuu49, vuu50, vuu51, True, bbg) → new_span2Zs11(vuu49, vuu50, vuu51, new_span2Ys0(vuu49, vuu51, bbg), new_span2Zs0(vuu49, vuu51, bbg), bbg)
new_groupByZs00(vuu18, vuu19, vuu20, True, bb) → new_span2Zs0(vuu18, vuu20, bb)
new_groupByZs0(vuu30, :(vuu310, vuu311), ba) → new_groupByZs00(vuu30, vuu310, vuu311, new_esEs28(vuu30, vuu310, ba), ba)
new_span2Ys0(vuu9, [], ce) → []
new_span2Ys0(vuu9, :(vuu110, vuu111), ce) → new_span2Ys10(vuu9, vuu110, vuu111, new_esEs5(vuu9, vuu110, ce), ce)
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
Q DP problem:
P is empty.
The TRS R consists of the following rules:
new_esEs4(vuu18, vuu200, app(app(app(ty_@3, bg), bh), ca)) → new_esEs14(vuu18, vuu200, bg, bh, ca)
new_esEs21(vuu301, vuu3101, ty_@0) → new_esEs13(vuu301, vuu3101)
new_esEs22(vuu300, vuu3100, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs19(True, False) → False
new_esEs19(False, True) → False
new_esEs5(vuu9, vuu110, app(ty_Ratio, da)) → new_esEs11(vuu9, vuu110, da)
new_esEs27(vuu300, vuu3100, app(ty_[], cag)) → new_esEs16(vuu300, vuu3100, cag)
new_primPlusNat1(Succ(vuu5700), Succ(vuu3101000)) → Succ(Succ(new_primPlusNat1(vuu5700, vuu3101000)))
new_esEs21(vuu301, vuu3101, ty_Double) → new_esEs17(vuu301, vuu3101)
new_esEs25(vuu302, vuu3102, app(ty_[], bgc)) → new_esEs16(vuu302, vuu3102, bgc)
new_primEqInt(Neg(Succ(vuu3000)), Pos(vuu3100)) → False
new_primEqInt(Pos(Succ(vuu3000)), Neg(vuu3100)) → False
new_esEs25(vuu302, vuu3102, ty_Bool) → new_esEs19(vuu302, vuu3102)
new_esEs25(vuu302, vuu3102, ty_Char) → new_esEs8(vuu302, vuu3102)
new_esEs25(vuu302, vuu3102, app(ty_Ratio, bfd)) → new_esEs11(vuu302, vuu3102, bfd)
new_esEs25(vuu302, vuu3102, ty_@0) → new_esEs13(vuu302, vuu3102)
new_esEs15(Left(vuu300), Right(vuu3100), ha, ff) → False
new_esEs15(Right(vuu300), Left(vuu3100), ha, ff) → False
new_esEs18(Float(vuu300, vuu301), Float(vuu3100, vuu3101)) → new_esEs9(new_sr(vuu300, vuu3100), new_sr(vuu301, vuu3101))
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(app(ty_Either, baa), bab)) → new_esEs15(vuu300, vuu3100, baa, bab)
new_esEs26(vuu301, vuu3101, ty_Int) → new_esEs9(vuu301, vuu3101)
new_esEs27(vuu300, vuu3100, app(ty_Ratio, bhh)) → new_esEs11(vuu300, vuu3100, bhh)
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(ty_Ratio, hd)) → new_esEs11(vuu300, vuu3100, hd)
new_primEqInt(Neg(Zero), Pos(Succ(vuu31000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vuu31000))) → False
new_esEs13(@0, @0) → True
new_span2Ys10(vuu40, vuu41, vuu42, False, fd) → []
new_esEs12(Just(vuu300), Just(vuu3100), app(app(ty_@2, bae), baf)) → new_esEs7(vuu300, vuu3100, bae, baf)
new_esEs27(vuu300, vuu3100, app(app(ty_@2, bhf), bhg)) → new_esEs7(vuu300, vuu3100, bhf, bhg)
new_esEs20(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), app(app(ty_Either, gf), gg), ff) → new_esEs15(vuu300, vuu3100, gf, gg)
new_esEs22(vuu300, vuu3100, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs26(vuu301, vuu3101, app(ty_Maybe, bgg)) → new_esEs12(vuu301, vuu3101, bgg)
new_esEs22(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_primMulNat0(Zero, Zero) → Zero
new_esEs28(vuu30, vuu310, ty_Bool) → new_esEs19(vuu30, vuu310)
new_esEs28(vuu30, vuu310, ty_Ordering) → new_esEs10(vuu30, vuu310)
new_esEs22(vuu300, vuu3100, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs21(vuu301, vuu3101, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs14(vuu301, vuu3101, bdb, bdc, bdd)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Float, ff) → new_esEs18(vuu300, vuu3100)
new_esEs7(@2(vuu300, vuu301), @2(vuu3100, vuu3101), bbh, bca) → new_asAs(new_esEs22(vuu300, vuu3100, bbh), new_esEs21(vuu301, vuu3101, bca))
new_esEs26(vuu301, vuu3101, app(ty_[], bhe)) → new_esEs16(vuu301, vuu3101, bhe)
new_esEs21(vuu301, vuu3101, app(app(ty_Either, bde), bdf)) → new_esEs15(vuu301, vuu3101, bde, bdf)
new_esEs28(vuu30, vuu310, app(ty_[], ea)) → new_esEs16(vuu30, vuu310, ea)
new_primPlusNat0(Zero, vuu310100) → Succ(vuu310100)
new_esEs4(vuu18, vuu200, ty_Ordering) → new_esEs10(vuu18, vuu200)
new_esEs6(Integer(vuu300), Integer(vuu3100)) → new_primEqInt(vuu300, vuu3100)
new_esEs4(vuu18, vuu200, app(ty_Ratio, be)) → new_esEs11(vuu18, vuu200, be)
new_esEs28(vuu30, vuu310, ty_Integer) → new_esEs6(vuu30, vuu310)
new_esEs5(vuu9, vuu110, app(app(app(ty_@3, dc), dd), de)) → new_esEs14(vuu9, vuu110, dc, dd, de)
new_esEs25(vuu302, vuu3102, ty_Float) → new_esEs18(vuu302, vuu3102)
new_esEs16(:(vuu300, vuu301), :(vuu3100, vuu3101), ea) → new_asAs(new_esEs20(vuu300, vuu3100, ea), new_esEs16(vuu301, vuu3101, ea))
new_esEs26(vuu301, vuu3101, ty_Ordering) → new_esEs10(vuu301, vuu3101)
new_sr(Neg(vuu3010), Pos(vuu31010)) → Neg(new_primMulNat0(vuu3010, vuu31010))
new_sr(Pos(vuu3010), Neg(vuu31010)) → Neg(new_primMulNat0(vuu3010, vuu31010))
new_esEs15(Left(vuu300), Left(vuu3100), ty_Char, ff) → new_esEs8(vuu300, vuu3100)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs25(vuu302, vuu3102, app(app(ty_Either, bga), bgb)) → new_esEs15(vuu302, vuu3102, bga, bgb)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Int, ff) → new_esEs9(vuu300, vuu3100)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, ty_Integer) → new_esEs6(vuu9, vuu110)
new_esEs12(Just(vuu300), Just(vuu3100), ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, app(ty_Ratio, ed)) → new_esEs11(vuu300, vuu3100, ed)
new_esEs12(Just(vuu300), Just(vuu3100), app(app(ty_Either, bbd), bbe)) → new_esEs15(vuu300, vuu3100, bbd, bbe)
new_esEs22(vuu300, vuu3100, app(ty_[], bfa)) → new_esEs16(vuu300, vuu3100, bfa)
new_groupByZs00(vuu18, vuu19, vuu20, False, bb) → :(vuu19, vuu20)
new_esEs26(vuu301, vuu3101, ty_Float) → new_esEs18(vuu301, vuu3101)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs14(@3(vuu300, vuu301, vuu302), @3(vuu3100, vuu3101, vuu3102), bcc, bcd, bce) → new_asAs(new_esEs27(vuu300, vuu3100, bcc), new_asAs(new_esEs26(vuu301, vuu3101, bcd), new_esEs25(vuu302, vuu3102, bce)))
new_esEs26(vuu301, vuu3101, ty_Integer) → new_esEs6(vuu301, vuu3101)
new_esEs4(vuu18, vuu200, app(app(ty_Either, cb), cc)) → new_esEs15(vuu18, vuu200, cb, cc)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Double, ff) → new_esEs17(vuu300, vuu3100)
new_primEqNat0(Zero, Succ(vuu31000)) → False
new_primEqNat0(Succ(vuu3000), Zero) → False
new_esEs21(vuu301, vuu3101, ty_Int) → new_esEs9(vuu301, vuu3101)
new_esEs26(vuu301, vuu3101, app(app(ty_@2, bgd), bge)) → new_esEs7(vuu301, vuu3101, bgd, bge)
new_groupByZs0(vuu30, :(vuu310, vuu311), ba) → new_groupByZs00(vuu30, vuu310, vuu311, new_esEs28(vuu30, vuu310, ba), ba)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs4(vuu18, vuu200, ty_Float) → new_esEs18(vuu18, vuu200)
new_esEs25(vuu302, vuu3102, app(app(ty_@2, bfb), bfc)) → new_esEs7(vuu302, vuu3102, bfb, bfc)
new_esEs4(vuu18, vuu200, ty_Bool) → new_esEs19(vuu18, vuu200)
new_esEs23(vuu301, vuu3101, ty_Integer) → new_esEs6(vuu301, vuu3101)
new_esEs22(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs21(vuu301, vuu3101, app(ty_Maybe, bda)) → new_esEs12(vuu301, vuu3101, bda)
new_esEs16([], :(vuu3100, vuu3101), ea) → False
new_esEs16(:(vuu300, vuu301), [], ea) → False
new_esEs28(vuu30, vuu310, ty_Float) → new_esEs18(vuu30, vuu310)
new_span2Zs0(vuu18, [], bb) → []
new_esEs5(vuu9, vuu110, ty_Ordering) → new_esEs10(vuu9, vuu110)
new_esEs5(vuu9, vuu110, ty_Float) → new_esEs18(vuu9, vuu110)
new_esEs28(vuu30, vuu310, ty_@0) → new_esEs13(vuu30, vuu310)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs26(vuu301, vuu3101, ty_@0) → new_esEs13(vuu301, vuu3101)
new_esEs15(Left(vuu300), Left(vuu3100), app(ty_[], gh), ff) → new_esEs16(vuu300, vuu3100, gh)
new_esEs24(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_esEs27(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs25(vuu302, vuu3102, ty_Integer) → new_esEs6(vuu302, vuu3102)
new_esEs26(vuu301, vuu3101, ty_Char) → new_esEs8(vuu301, vuu3101)
new_span2Zs11(vuu49, vuu50, vuu51, vuu56, vuu55, bbg) → vuu55
new_esEs21(vuu301, vuu3101, ty_Float) → new_esEs18(vuu301, vuu3101)
new_esEs4(vuu18, vuu200, ty_@0) → new_esEs13(vuu18, vuu200)
new_esEs26(vuu301, vuu3101, ty_Double) → new_esEs17(vuu301, vuu3101)
new_esEs4(vuu18, vuu200, ty_Integer) → new_esEs6(vuu18, vuu200)
new_span2Ys11(vuu40, vuu41, vuu42, vuu54, vuu53, fd) → :(vuu41, vuu54)
new_groupByZs0(vuu30, [], ba) → []
new_groupByZs00(vuu18, vuu19, vuu20, True, bb) → new_span2Zs0(vuu18, vuu20, bb)
new_esEs12(Just(vuu300), Just(vuu3100), app(ty_Ratio, bag)) → new_esEs11(vuu300, vuu3100, bag)
new_esEs22(vuu300, vuu3100, ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs25(vuu302, vuu3102, ty_Double) → new_esEs17(vuu302, vuu3102)
new_sr(Neg(vuu3010), Neg(vuu31010)) → Pos(new_primMulNat0(vuu3010, vuu31010))
new_esEs10(LT, LT) → True
new_esEs10(EQ, GT) → False
new_esEs10(GT, EQ) → False
new_esEs27(vuu300, vuu3100, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, app(ty_[], fc)) → new_esEs16(vuu300, vuu3100, fc)
new_esEs12(Just(vuu300), Nothing, bad) → False
new_esEs12(Nothing, Just(vuu3100), bad) → False
new_sr(Pos(vuu3010), Pos(vuu31010)) → Pos(new_primMulNat0(vuu3010, vuu31010))
new_asAs(False, vuu34) → False
new_esEs27(vuu300, vuu3100, app(ty_Maybe, caa)) → new_esEs12(vuu300, vuu3100, caa)
new_primEqNat0(Zero, Zero) → True
new_esEs20(vuu300, vuu3100, app(ty_Maybe, ee)) → new_esEs12(vuu300, vuu3100, ee)
new_primMulNat0(Zero, Succ(vuu310100)) → Zero
new_primMulNat0(Succ(vuu30100), Zero) → Zero
new_esEs15(Left(vuu300), Left(vuu3100), app(app(app(ty_@3, gc), gd), ge), ff) → new_esEs14(vuu300, vuu3100, gc, gd, ge)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Integer, ff) → new_esEs6(vuu300, vuu3100)
new_span2Zs10(vuu49, vuu50, vuu51, False, bbg) → :(vuu50, vuu51)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Int) → new_esEs9(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), app(ty_Maybe, gb), ff) → new_esEs12(vuu300, vuu3100, gb)
new_esEs10(GT, GT) → True
new_esEs25(vuu302, vuu3102, ty_Ordering) → new_esEs10(vuu302, vuu3102)
new_esEs4(vuu18, vuu200, app(ty_Maybe, bf)) → new_esEs12(vuu18, vuu200, bf)
new_esEs23(vuu301, vuu3101, ty_Int) → new_esEs9(vuu301, vuu3101)
new_esEs22(vuu300, vuu3100, app(app(ty_@2, bdh), bea)) → new_esEs7(vuu300, vuu3100, bdh, bea)
new_esEs12(Nothing, Nothing, bad) → True
new_esEs19(True, True) → True
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(ty_[], bac)) → new_esEs16(vuu300, vuu3100, bac)
new_esEs27(vuu300, vuu3100, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs27(vuu300, vuu3100, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(app(app(ty_@3, hf), hg), hh)) → new_esEs14(vuu300, vuu3100, hf, hg, hh)
new_esEs5(vuu9, vuu110, ty_@0) → new_esEs13(vuu9, vuu110)
new_primPlusNat0(Succ(vuu570), vuu310100) → Succ(Succ(new_primPlusNat1(vuu570, vuu310100)))
new_esEs5(vuu9, vuu110, ty_Int) → new_esEs9(vuu9, vuu110)
new_esEs20(vuu300, vuu3100, app(app(app(ty_@3, ef), eg), eh)) → new_esEs14(vuu300, vuu3100, ef, eg, eh)
new_esEs25(vuu302, vuu3102, app(ty_Maybe, bfe)) → new_esEs12(vuu302, vuu3102, bfe)
new_esEs15(Left(vuu300), Left(vuu3100), app(ty_Ratio, ga), ff) → new_esEs11(vuu300, vuu3100, ga)
new_esEs28(vuu30, vuu310, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs14(vuu30, vuu310, bcc, bcd, bce)
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(app(ty_@2, hb), hc)) → new_esEs7(vuu300, vuu3100, hb, hc)
new_esEs15(Left(vuu300), Left(vuu3100), ty_@0, ff) → new_esEs13(vuu300, vuu3100)
new_primEqInt(Neg(Succ(vuu3000)), Neg(Succ(vuu31000))) → new_primEqNat0(vuu3000, vuu31000)
new_esEs10(EQ, EQ) → True
new_esEs4(vuu18, vuu200, ty_Double) → new_esEs17(vuu18, vuu200)
new_esEs27(vuu300, vuu3100, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs20(vuu300, vuu3100, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs21(vuu301, vuu3101, ty_Ordering) → new_esEs10(vuu301, vuu3101)
new_primPlusNat1(Zero, Succ(vuu3101000)) → Succ(vuu3101000)
new_primPlusNat1(Succ(vuu5700), Zero) → Succ(vuu5700)
new_esEs16([], [], ea) → True
new_esEs28(vuu30, vuu310, app(app(ty_Either, ha), ff)) → new_esEs15(vuu30, vuu310, ha, ff)
new_esEs5(vuu9, vuu110, ty_Bool) → new_esEs19(vuu9, vuu110)
new_esEs4(vuu18, vuu200, ty_Char) → new_esEs8(vuu18, vuu200)
new_esEs21(vuu301, vuu3101, ty_Char) → new_esEs8(vuu301, vuu3101)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_span2Ys0(vuu9, [], ce) → []
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs19(False, False) → True
new_esEs21(vuu301, vuu3101, app(app(ty_@2, bcf), bcg)) → new_esEs7(vuu301, vuu3101, bcf, bcg)
new_esEs28(vuu30, vuu310, ty_Int) → new_esEs9(vuu30, vuu310)
new_esEs27(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs10(LT, GT) → False
new_esEs10(GT, LT) → False
new_primEqInt(Neg(Zero), Neg(Succ(vuu31000))) → False
new_primEqInt(Neg(Succ(vuu3000)), Neg(Zero)) → False
new_esEs15(Right(vuu300), Right(vuu3100), ha, app(ty_Maybe, he)) → new_esEs12(vuu300, vuu3100, he)
new_esEs22(vuu300, vuu3100, app(ty_Maybe, bec)) → new_esEs12(vuu300, vuu3100, bec)
new_esEs28(vuu30, vuu310, app(ty_Ratio, bcb)) → new_esEs11(vuu30, vuu310, bcb)
new_span2Ys10(vuu40, vuu41, vuu42, True, fd) → new_span2Ys11(vuu40, vuu41, vuu42, new_span2Ys0(vuu40, vuu42, fd), new_span2Zs0(vuu40, vuu42, fd), fd)
new_esEs26(vuu301, vuu3101, app(ty_Ratio, bgf)) → new_esEs11(vuu301, vuu3101, bgf)
new_esEs10(LT, EQ) → False
new_esEs10(EQ, LT) → False
new_esEs20(vuu300, vuu3100, app(app(ty_@2, eb), ec)) → new_esEs7(vuu300, vuu3100, eb, ec)
new_esEs21(vuu301, vuu3101, ty_Integer) → new_esEs6(vuu301, vuu3101)
new_esEs28(vuu30, vuu310, ty_Double) → new_esEs17(vuu30, vuu310)
new_esEs12(Just(vuu300), Just(vuu3100), app(ty_Maybe, bah)) → new_esEs12(vuu300, vuu3100, bah)
new_esEs20(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, app(app(ty_Either, beg), beh)) → new_esEs15(vuu300, vuu3100, beg, beh)
new_esEs5(vuu9, vuu110, app(ty_Maybe, db)) → new_esEs12(vuu9, vuu110, db)
new_esEs4(vuu18, vuu200, app(ty_[], cd)) → new_esEs16(vuu18, vuu200, cd)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs26(vuu301, vuu3101, app(app(app(ty_@3, bgh), bha), bhb)) → new_esEs14(vuu301, vuu3101, bgh, bha, bhb)
new_esEs12(Just(vuu300), Just(vuu3100), app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs14(vuu300, vuu3100, bba, bbb, bbc)
new_span2Ys0(vuu9, :(vuu110, vuu111), ce) → new_span2Ys10(vuu9, vuu110, vuu111, new_esEs5(vuu9, vuu110, ce), ce)
new_asAs(True, vuu34) → vuu34
new_esEs27(vuu300, vuu3100, ty_Char) → new_esEs8(vuu300, vuu3100)
new_primMulNat0(Succ(vuu30100), Succ(vuu310100)) → new_primPlusNat0(new_primMulNat0(vuu30100, Succ(vuu310100)), vuu310100)
new_esEs28(vuu30, vuu310, app(app(ty_@2, bbh), bca)) → new_esEs7(vuu30, vuu310, bbh, bca)
new_esEs28(vuu30, vuu310, app(ty_Maybe, bad)) → new_esEs12(vuu30, vuu310, bad)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Int) → new_esEs9(vuu300, vuu3100)
new_primEqInt(Pos(Succ(vuu3000)), Pos(Succ(vuu31000))) → new_primEqNat0(vuu3000, vuu31000)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Ordering, ff) → new_esEs10(vuu300, vuu3100)
new_span2Zs0(vuu18, :(vuu200, vuu201), bb) → new_span2Zs10(vuu18, vuu200, vuu201, new_esEs4(vuu18, vuu200, bb), bb)
new_esEs22(vuu300, vuu3100, ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, app(ty_[], dh)) → new_esEs16(vuu9, vuu110, dh)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs26(vuu301, vuu3101, ty_Bool) → new_esEs19(vuu301, vuu3101)
new_esEs5(vuu9, vuu110, app(app(ty_@2, cf), cg)) → new_esEs7(vuu9, vuu110, cf, cg)
new_esEs11(:%(vuu300, vuu301), :%(vuu3100, vuu3101), bcb) → new_asAs(new_esEs24(vuu300, vuu3100, bcb), new_esEs23(vuu301, vuu3101, bcb))
new_esEs25(vuu302, vuu3102, ty_Int) → new_esEs9(vuu302, vuu3102)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Float) → new_esEs18(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, app(app(app(ty_@3, bed), bee), bef)) → new_esEs14(vuu300, vuu3100, bed, bee, bef)
new_esEs8(Char(vuu300), Char(vuu3100)) → new_primEqNat0(vuu300, vuu3100)
new_primEqNat0(Succ(vuu3000), Succ(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs9(vuu30, vuu310) → new_primEqInt(vuu30, vuu310)
new_esEs25(vuu302, vuu3102, app(app(app(ty_@3, bff), bfg), bfh)) → new_esEs14(vuu302, vuu3102, bff, bfg, bfh)
new_esEs5(vuu9, vuu110, ty_Double) → new_esEs17(vuu9, vuu110)
new_esEs28(vuu30, vuu310, ty_Char) → new_esEs8(vuu30, vuu310)
new_esEs24(vuu300, vuu3100, ty_Integer) → new_esEs6(vuu300, vuu3100)
new_esEs27(vuu300, vuu3100, app(app(app(ty_@3, cab), cac), cad)) → new_esEs14(vuu300, vuu3100, cab, cac, cad)
new_esEs4(vuu18, vuu200, ty_Int) → new_esEs9(vuu18, vuu200)
new_esEs20(vuu300, vuu3100, ty_Char) → new_esEs8(vuu300, vuu3100)
new_esEs15(Left(vuu300), Left(vuu3100), app(app(ty_@2, fg), fh), ff) → new_esEs7(vuu300, vuu3100, fg, fh)
new_esEs15(Left(vuu300), Left(vuu3100), ty_Bool, ff) → new_esEs19(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, ty_Char) → new_esEs8(vuu9, vuu110)
new_esEs21(vuu301, vuu3101, app(ty_Ratio, bch)) → new_esEs11(vuu301, vuu3101, bch)
new_esEs21(vuu301, vuu3101, app(ty_[], bdg)) → new_esEs16(vuu301, vuu3101, bdg)
new_esEs27(vuu300, vuu3100, app(app(ty_Either, cae), caf)) → new_esEs15(vuu300, vuu3100, cae, caf)
new_esEs12(Just(vuu300), Just(vuu3100), ty_Ordering) → new_esEs10(vuu300, vuu3100)
new_span2Zs10(vuu49, vuu50, vuu51, True, bbg) → new_span2Zs11(vuu49, vuu50, vuu51, new_span2Ys0(vuu49, vuu51, bbg), new_span2Zs0(vuu49, vuu51, bbg), bbg)
new_esEs20(vuu300, vuu3100, ty_@0) → new_esEs13(vuu300, vuu3100)
new_esEs5(vuu9, vuu110, app(app(ty_Either, df), dg)) → new_esEs15(vuu9, vuu110, df, dg)
new_esEs20(vuu300, vuu3100, app(app(ty_Either, fa), fb)) → new_esEs15(vuu300, vuu3100, fa, fb)
new_esEs27(vuu300, vuu3100, ty_Bool) → new_esEs19(vuu300, vuu3100)
new_esEs22(vuu300, vuu3100, app(ty_Ratio, beb)) → new_esEs11(vuu300, vuu3100, beb)
new_primEqInt(Pos(Zero), Pos(Succ(vuu31000))) → False
new_primEqInt(Pos(Succ(vuu3000)), Pos(Zero)) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs26(vuu301, vuu3101, app(app(ty_Either, bhc), bhd)) → new_esEs15(vuu301, vuu3101, bhc, bhd)
new_esEs21(vuu301, vuu3101, ty_Bool) → new_esEs19(vuu301, vuu3101)
new_esEs15(Right(vuu300), Right(vuu3100), ha, ty_Double) → new_esEs17(vuu300, vuu3100)
new_esEs17(Double(vuu300, vuu301), Double(vuu3100, vuu3101)) → new_esEs9(new_sr(vuu300, vuu3100), new_sr(vuu301, vuu3101))
new_esEs12(Just(vuu300), Just(vuu3100), app(ty_[], bbf)) → new_esEs16(vuu300, vuu3100, bbf)
new_esEs4(vuu18, vuu200, app(app(ty_@2, bc), bd)) → new_esEs7(vuu18, vuu200, bc, bd)
The set Q consists of the following terms:
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Just(x0), Just(x1), ty_Char)
new_esEs15(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs15(Left(x0), Left(x1), ty_Int, x2)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_@0)
new_esEs13(@0, @0)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(Just(x0), Just(x1), app(ty_[], x2))
new_primPlusNat1(Zero, Succ(x0))
new_esEs15(Left(x0), Left(x1), app(ty_[], x2), x3)
new_span2Zs11(x0, x1, x2, x3, x4, x5)
new_esEs12(Just(x0), Just(x1), ty_Integer)
new_esEs28(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Bool)
new_esEs28(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs25(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs28(x0, x1, ty_Int)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Char)
new_groupByZs0(x0, [], x1)
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Integer)
new_esEs5(x0, x1, ty_Integer)
new_esEs8(Char(x0), Char(x1))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(False, False)
new_esEs22(x0, x1, ty_Char)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs15(Right(x0), Right(x1), x2, ty_Bool)
new_esEs12(Nothing, Just(x0), x1)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primEqInt(Neg(Zero), Neg(Zero))
new_groupByZs00(x0, x1, x2, True, x3)
new_esEs12(Just(x0), Nothing, x1)
new_esEs28(x0, x1, ty_Bool)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs12(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Double)
new_span2Zs10(x0, x1, x2, False, x3)
new_esEs4(x0, x1, ty_Bool)
new_esEs20(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Integer)
new_esEs15(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs12(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs10(GT, EQ)
new_esEs10(EQ, GT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(Just(x0), Just(x1), ty_Ordering)
new_esEs11(:%(x0, x1), :%(x2, x3), x4)
new_esEs20(x0, x1, ty_Float)
new_esEs15(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(EQ, LT)
new_esEs10(LT, EQ)
new_esEs28(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_span2Zs0(x0, [], x1)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Integer)
new_primMulNat0(Zero, Succ(x0))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs15(Right(x0), Right(x1), x2, ty_@0)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs15(Left(x0), Right(x1), x2, x3)
new_esEs15(Right(x0), Left(x1), x2, x3)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_@0)
new_esEs10(LT, LT)
new_esEs25(x0, x1, ty_Integer)
new_esEs5(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Integer)
new_esEs15(Right(x0), Right(x1), x2, ty_Integer)
new_esEs25(x0, x1, ty_Ordering)
new_esEs15(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs26(x0, x1, app(ty_[], x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs15(Left(x0), Left(x1), ty_Float, x2)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Int)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs15(Left(x0), Left(x1), ty_@0, x2)
new_esEs16([], :(x0, x1), x2)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs19(True, True)
new_esEs12(Just(x0), Just(x1), ty_@0)
new_groupByZs00(x0, x1, x2, False, x3)
new_esEs22(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_@0)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_@0)
new_esEs15(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_sr(Neg(x0), Neg(x1))
new_esEs26(x0, x1, ty_Char)
new_esEs15(Left(x0), Left(x1), ty_Bool, x2)
new_primPlusNat0(Succ(x0), x1)
new_esEs28(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_Bool)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs15(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs5(x0, x1, ty_Float)
new_esEs15(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs15(Right(x0), Right(x1), x2, ty_Char)
new_esEs4(x0, x1, ty_Float)
new_primEqNat0(Zero, Zero)
new_primEqNat0(Zero, Succ(x0))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs12(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Int)
new_esEs18(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Integer)
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_esEs10(GT, GT)
new_sr(Pos(x0), Pos(x1))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs6(Integer(x0), Integer(x1))
new_esEs15(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs15(Right(x0), Right(x1), x2, ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs15(Right(x0), Right(x1), x2, ty_Int)
new_primMulNat0(Zero, Zero)
new_esEs5(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(:(x0, x1), :(x2, x3), x4)
new_esEs28(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Char)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Ordering)
new_esEs15(Left(x0), Left(x1), ty_Char, x2)
new_esEs12(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(x0, x1)
new_esEs25(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Float)
new_span2Ys0(x0, [], x1)
new_esEs16(:(x0, x1), [], x2)
new_esEs21(x0, x1, ty_Char)
new_esEs12(Just(x0), Just(x1), ty_Bool)
new_span2Ys0(x0, :(x1, x2), x3)
new_esEs10(GT, LT)
new_esEs10(LT, GT)
new_primMulNat0(Succ(x0), Zero)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Double)
new_esEs17(Double(x0, x1), Double(x2, x3))
new_esEs15(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs12(Just(x0), Just(x1), ty_Double)
new_esEs16([], [], x0)
new_esEs28(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_@0)
new_span2Ys10(x0, x1, x2, True, x3)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Int)
new_esEs14(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Int)
new_esEs28(x0, x1, ty_Float)
new_span2Ys11(x0, x1, x2, x3, x4, x5)
new_primEqNat0(Succ(x0), Zero)
new_esEs5(x0, x1, ty_Bool)
new_esEs15(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, ty_Bool)
new_esEs15(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_span2Zs10(x0, x1, x2, True, x3)
new_span2Zs0(x0, :(x1, x2), x3)
new_esEs19(False, True)
new_esEs19(True, False)
new_esEs15(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Bool)
new_esEs15(Left(x0), Left(x1), ty_Integer, x2)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Zero, Zero)
new_esEs5(x0, x1, ty_Double)
new_esEs15(Right(x0), Right(x1), x2, ty_Float)
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Int)
new_asAs(False, x0)
new_esEs22(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Double)
new_esEs15(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs10(EQ, EQ)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs26(x0, x1, ty_Double)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Ordering)
new_esEs12(Just(x0), Just(x1), ty_Float)
new_asAs(True, x0)
new_span2Ys10(x0, x1, x2, False, x3)
new_esEs7(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Bool)
new_esEs20(x0, x1, ty_Ordering)
new_groupByZs0(x0, :(x1, x2), x3)
new_esEs5(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Char)
new_esEs12(Nothing, Nothing, x0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs15(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs12(Just(x0), Just(x1), ty_Int)
new_esEs20(x0, x1, ty_Double)
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.